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 Field a, Heap = <a>[ref, Field a]a;
function IsHeap(Heap) returns (bool);
const alloc : Field bool;
axiom (forall H:Heap, o:ref, f:Field ref ::
IsHeap(H) && H[o,alloc] ==> H[H[o,f], alloc]);
procedure P() returns () {
var h : Heap, o : ref, g : Field ref, i : Field ref, o2 : ref;
assume IsHeap(h) && h[o, alloc];
o2 := h[o, g];
assert h[o2, alloc];
o2 := h[o2, g];
assert h[o2, alloc];
h[o2, alloc] := false;
o2 := h[o2, g];
assert h[o2, alloc]; // should not be provable
}
type ref;
|
