In this second part of the tutorial, we will be modelling a Map that associates unique keys with values (such as eg.

Map in Java) and show how Alloy can be used to explore dynamic behaviour.

The static aspects are easy to specify:

module examples/tutorial/Map

abstract sig Object {}

sig Key, Value extends Object {}

sig Map { values: Key -> Value }
As in Java,

abstract ensures that there cannot be any direct 'instances' of

Object. Similarly,

extends means that

Objects can either be

Keys or

Values, but not both.

values above is a

relation that represents the mapping of

Keys to

Values. This would be written in a schema in Object-Z as

values ⊆ K × V where K is the set of all Keys and V is the set of all Values.

We can visualize this model as before:

pred show() {}
run show for 2
The first instance produced by Alloy only consists of a

Key and a

Value but no

Map. We could browse through the various solutions until we find one that actually includes a

Map, however there is a better way.

As mentioned before, Alloy produces instances that satisfy the predicate passed to

run. We can add a constraint that specifies that there is at least one

Map:

pred show() { #Map > 0 }

run show for 2
We now get 2

Maps and one Value. To get exactly one

Map, we can either change the constraint to

#Map = 1
or we can modify the

run command as follows:

run show for 2 but exactly 1 Map
Next, let us check that the mapping of keys to values is unique. This can be done in Alloy via

assertions:

assert mappingIsUnique {

all m:Map, k:Key, v, v':Value |

k -> v in m.values and k -> v' in m.values implies v = v'

}
This says that if a

Map m maps a key

k to two values

v and

v' then they must be the same. Note how the relational product operator ("

->") in

k -> v is used to represent the tuple (k, v) and how

m.values is treated as a set of tuples

{(Key, Value)}. To check an assertion, we can use the command

check. As for

run, we have to specify the scope:

check mappingIsUnique for 2
If we execute this, Alloy searches all possible combinations of at most two objects of each signature for a counterexample that violates the assertion. Since it cannot find one, it tells us that the assertion may be valid. However, if we increase the scope to three, it produces the following:

To make this even more obvious, we can ask Alloy to project over

Map using the Projection button:

We see that a key refers to two values. To fix this, we use the

lone keyword that we have already seen:

sig Map { values: Key -> lone Value }

Now, the assertion holds even if we increase the scope to 15 (say). This produces a much larger coverage than any testcase ever could and gives us a high level of confidence that the assertion may be valid.

Finally, to make the instances of later steps less verbose, we include the constraint that all keys (and values) belong to some

Map:

fact {

all k:Key | some v:Value, m:Map | k -> v in m.values

all v:Value | some k:Key, m:Map | k -> v in m.values

}
Note that, unlike in the Queue example, it makes sense for a key/value to belong to more than one

Map. Also observe that the fact above is anonymous; Alloy does not require you to provide a name.

We have now developed the static aspects of the

Map. In the next section we will continue to develop the dynamics of our example.