References and Containment

Experimental
1

My use case for Alloy is probably a bit different from academics. I am not so much interested in proving something is correct since I know developers can still screw up a perfect specification. A fact of life that is worsened by the often very difficult to understand models. I am trying to use Alloy as a description language.

Alloy’s relational model with an OO twist works very nice for this. However, one of the things I am struggling with is the reference and containment. In software, this distinction is quite crucial. In an Alloy model it seems to disappear. For example. in programs you often have an ID to another object. A significant amount of code is dedicated in managing this relation via the ID. So in Alloy, you can put an ID sig in your 'object`. However, this seems a lot of work and provides little value. I recall that Daniel recommends not to do this, just use the sig name. This is my current practice but now there is no longer a difference between a containment relation and a reference relation.

I’ve been experimenting with the syntax to see if I should have an operator indicating the reference relation on a field declaration:

  sig Foo {
        bar : contains Bar,
        kit  : set Kit
 }

I do not think it would make a huge difference in modeling but I guess that we could show this in the Viz view. (cardinalities would also be nice there!). I guess a containment would also indicate a disjoint relation and others can only refer to it by reference. These are quite important subtleties that require a lot of text to capture today.

Ideas?

2

Hi Peter,
what would be the exact semantics?
In any case, the question is whether this is a distinction we want to make at the Alloy level, or whether this is something you’d rather do in a formal framework which targets a software notation (such as UML).

3

Interesting question. This is the kind of distinction that has exercised data modelers for a long time, and I bet Kent discusses it in Data & Reality. As David asks, the question is: what semantic do you want? The usual interpretation of containment is that you get cascading deletes. Another possibility is that it means that the contained value is not shared. At one point in Alloy’s design, we tried various syntaxes that would have supported this in a decl, such as

sig Foo {
        lone bar : Bar,
        kit  : set Kit
 }

but decided it was too clunky and not much of a saving over writing

fact {bar: Foo lone -> Bar}

You might also have an even more expansive notion of containment in mind, where the field name is not relevant, and you want to say that each bar belongs to only one foo in any relation. Then the question would be whether you’d apply this also to integers, eg.

4

Primarily the containment would be useful in the mapping to software. The lack of this distinction between reference & containment requires the developer to make a random choice. As said, I see Alloy more and more as a language to describe.

That said, a containment would require disjunctiveness, probably not the right word, in the whole model, which I think could simplify the model. It might also be useful in the visualization.

5

I think I see what you mean. You’d need to handle value and reference Equality and that gets messy quickly.