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
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
|
type Field a;
function FieldAccessFun<b>(heap : <a>[ref, Field a]a, obj : ref, f : Field b)
returns (res:b);
procedure FieldAccess<b>(heap : <a>[ref, Field a]a, obj : ref, f : Field b)
returns (res:b) {
start:
res := heap[f, obj]; // error: wrong argument order
res := heap[obj, f];
assert res == FieldAccessFun(heap, obj, f);
return;
}
procedure UseHeap(heap : <a>[ref, Field a]a) {
var f1 : Field int; var f2 : Field bool; var obj : ref;
var x : int; var y : bool;
call x := FieldAccess(heap, f1, obj); // error: wrong argument order
call x := FieldAccess(heap, obj, f1);
call y := FieldAccess(heap, obj, f2);
call y := FieldAccess(heap, obj, f1); // error: wrong result type
call x := FieldAccess(heap, obj, obj); // error: wrong argument type
}
procedure injective<b>(heap : <a>[ref, Field a]a, obj0 : ref, obj1 : ref, f : Field b);
requires obj0 != obj1;
ensures heap[obj0, f] != heap[obj1, f];
procedure testCallForall(heap : <a>[ref, Field a]a) {
var f1 : Field int; var f2 : Field bool;
start:
call forall injective(heap, *, *, f1);
call forall injective(heap, *, *, f2);
call forall injective(heap, *, *, *);
call forall injective(heap, *, f1, *); // error: wrong argument type
}
type ref;
|
