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
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
|
const a: [int]bool;
// element 5 of a stores the value true
axiom a == a[5 := true];
procedure P()
{
assert a[5];
}
procedure Q()
{
assert a[4]; // error
}
procedure R()
{
assert !a[5]; // error
}
procedure S(y: int, t: bool)
requires y <= 5;
{
if (a[y := t][5] == false) {
assert y == 5;
}
}
procedure T0(aa: [int,ref]bool)
{
assert aa[5,null := true] != aa[2,null := false]; // error
}
procedure T1(aa: [int,ref]bool)
requires aa[5,null] && !aa[2,null];
{
assert aa[5,null := true] == aa[2,null := false]; // error, because we have no extensionality
}
procedure T2(aa: [int,ref]bool)
requires aa[5,null] && !aa[2,null];
{
assert (forall x: int, y: ref :: aa[5,null := true][x,y] == aa[2,null := false][x,y]);
}
procedure U0(a: [int]int)
{
var b: [int]int;
b := a[5 := 12];
assert a == b; // error
}
procedure U1() returns (a: [int]int)
{
var b: [int]int;
b := a[5 := 12];
a[5] := 12;
assert a == b;
}
type Field a;
const unique IntField: Field int;
const unique RefField: Field ref;
const unique SomeField: Field int;
procedure FieldProc(H: <a>[ref,Field a]a, this: ref)
{
var i: int, r: ref, y: any;
var K: <a>[ref,Field a]a;
K := H[this, IntField := 5][this, RefField := null][this, SomeField := 100][this, IntField := 7];
assert K[this, IntField] == 7;
assert K[this, RefField] == null;
assert K[this, SomeField] == 100;
}
type ref, any;
const null : ref;
|
