We will proceed to adding dynamic behaviour to our model. In particular, we will define the operation of adding entries to the
Map:
pred put(m, m':Map, k:Key, v:Value) { m'.values = m.values + k -> v }
This is very similar to an operation schema in Object-Z: the instances of
put consist of the state before(
m), inputs(
v), state after(
m') and outputs of the operation. As in Object-Z, the convention is to use
' to decorate the state after the operation.
+ is the
set union operator. The above constraint therefore reads as:
"The set of values after is equal to the union of the set of values before with the extra mapping from k to v"
(Note how
m.values is again treated as a set of tuples).
We execute this predicate with the usual command:
run put for 3 but exactly 2 Map, exactly 1 Key, exactly 1 Value
Alloy produces the following instance which illustrates the functionality of the
put operation:
module examples/tutorial/Map
abstract sig Object {}
sig Key, Value extends Object {}
sig Map {
values: Key -> lone Value
}
assert mappingIsUnique {
all m:Map, k:Key, v, v':Value |
k -> v in m.values
and k -> v' in m.values
implies v = v'
}
pred put(m, m':Map, k:Key, v:Value) {
m'.values = m.values + k -> v
}
run put for 3 but exactly 2 Map,
exactly 1 Key, exactly 1 Value
|
State before
|
State after
|
The assertion
putLocal checks that
put does not change the existing mappings in the set:
assert putLocal {
all m, m': Map, k, k': Key, v: Value |
put[m,m',k,v] and k != k' implies
lookup[m,k'] = lookup[m',k']
}
fun lookup(m: Map, k: Key): set Value { k.(m.values) }
lookup is an example of a
function in Alloy. It uses the
. operator to return all values that are associated with the
Key k in the
Map m, i.e. the set
{v | (k, v) in m.values}. Note that the arguments to a function are enclosed in square brackets
[]. This is new in Alloy 4; in older versions (such as the one used in the official tutorial on the MIT website), they were enclosed in parentheses ().
We check that the assertion holds as before:
check putLocal
Alloy informs us that no counter-examples were found. This is also the case if we increase the scope (to 15, say). Confident that our assertion may be valid, we stop here.
This already marks the end of our short tutorial. If you want to learn more about Alloy, we suggest looking at the following excellent resources: