How to think about an Alloy model: 3 levels
There are three basic levels of abstraction at which you can read an
Alloy model.
- 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.
sig S extends E {
F: one T
}
fact {
all s:S | s.F in T
}
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 exactly one 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 and relations,
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.
- 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