How to think about an Alloy model: 3 levels

• The highest level of abstraction is the OO paradigm. This level is helpful for getting started and for understanding a model at a glance; the syntax is probably familiar to you and usually does what you'd expect it to do.
• The middle level of abstraction is set theory. You will probably find yourself using this level of understanding the most (although the OO level will still be useful).
• The lowest level of abstraction is atoms and relations, and corresponds to the true semantics of the language. However, even advanced users rarely think about things this way.

Consider the following excerpt. A signature sig S, extending E, has a field F of type T. Elsewhere in the model, the expression "s.F" appears.

we write:

  sig S extends E {
    F:T
  }

  fact {
    all s:S | s.F in X
  }

The fragment can be roughly interpreted in an Object Oriented sense.

• S is a class
• S extends its superclass E
• F is a field of S pointing to a T
• s is an instance of S
• . accesses a field
• s.F returns something of type T

The fragment can be safely read as being about sets, elements, and relations among those sets and elements. Most users find this way of thinking intuitive after a little practice and does not lead to errors as the OO approach occasionally does.

• S is a set (and so is E)
• S is a subset of E
• F is a relation which maps each S to some T
• s is an element of S
• . composes relations
• s.F composes the unary relation s with the binary relations F, returning a unary relation of type T

In some sense, we are modeling a field of a class as a relation which maps instances of that class to instances of that field.

The technical meaning is in terms of atoms [link to atoms] and relations [link to everything is a relation, and is rather hairy. Most users do not need this level of understanding most of the time, but you may be curious about how things are working on the inside. A more thorough discussion of this can be found in the reference manual.

• S is an atom (and so is E)
• the containment relation maps E to S (among other things it does)
• F is a relation from S to T
• the containment relation maps S to s (among other things)
• . composes relations
• s.F composes the unary relation s with the binary relations F, resulting in a unary relation t, such that the containment relation maps T to t

[diagram of composition as matrix multiplication]

related sidenotes:

• operational and declarative paradigms described in greater detail.
• pretending alloy is OO
• interpreting the compose operator (.) ("relational join")

list all sidenotes

clear this sidenote