1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
type Set = <a> [a] bool;
type Field a;
type Heap = <b> [ref, Field b] b;
const emptySet : Set;
axiom (forall<t> x:t :: !emptySet[x]);
procedure P() returns () {
var x : Set, f : Field Set, g : Field int, heap : Heap, o : ref;
x := emptySet;
heap[o, f] := x;
heap[o, g] := 13;
assert heap[o, f] == emptySet && heap[o, g] == 13;
heap[o, f] := heap[o, f][17 := true];
heap[o, f] := heap[o, f][g := true];
assert (forall<t> y:t :: heap[o, f][y] == (y == 17 || y == g));
assert (forall<t> y:t :: heap[o, f][y] == (y == 16 || y == g)); // should not hold
}
type ref;
|
