Pretending Alloy is Object Oriented ("OO")

Several clever definitions of Alloy language constructs allow you to write models which look like a lot like Java/C++ OO code. The key to getting this to work is the interpretation of signature declarations (a "sig" statements) and the "." operator (relational composition). Signatures are technically sets, but they can be thought of as objects in the OO paradigm.

Consider the following excerpt. A signature sig S, extending E, has a field F of type T.

we write:

  sig S extends E {
    F:T
  }

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

The fragment can be 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 OO interpretation can be helpful for understanding a model at a glance, but can be dangerous if you don't have any deeper understanding. As you become more familiar with Alloy, you will find yourself thinking in set theoretic terms.