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
82
83
84
85
86
87
88
89
90
91
|
class A {
// all of the following array types are allowed
var a: array<int>;
var b: array <bool>;
var c: array <A>;
var d: array1 <A>; // this is a synonym for array<A>
var e: array2 <A>;
var f: array3 <A>;
var g: array300 <A>;
var h: array3000 <array2<int>>;
method M0()
requires a != null && b != null;
modifies a;
{
if (5 <= a.Length && a.Length <= b.Length) {
var x := b[2];
var y := a[1];
var z := a[2];
a[2] := a[2] + 1;
assert x == b[2];
assert y == a[1];
assert z == a[2] - 1;
}
}
method M1()
requires a != null && d != null;
modifies a;
{
if (5 <= a.Length && a.Length <= d.Length) {
var x := d[2];
var y := a[1];
var z := a[2];
a[2] := a[2] + 1;
assert y == a[1];
assert z == a[2] - 1;
assert x == d[2]; // error: a and d may be equal
}
}
method M2(i: int, j: int, k: int, val: A)
requires f != null;
requires 0 <= i && i < f.Length0;
requires 0 <= j && j < f.Length1;
requires 0 <= k && k < f.Length2;
modifies f;
{
if (*) {
if (k < f.Length0) {
var save := f[k,j,k];
f[i,j,k] := val;
assert save == f[k,j,k]; // error: k and i may be equal
}
} else if (k < f.Length0 && k != i) {
if (k < f.Length0) {
var save := f[k,j,k];
f[i,j,k] := val;
assert save == f[k,j,k]; // fine
}
}
}
method M3(i: int, j: int, k: int)
requires f != null;
requires 0 <= i && i < f.Length0;
requires 0 <= j && j < f.Length1;
requires 0 <= k && k < f.Length2;
modifies f;
decreases i;
{
if (i != 0) {
var z := new A[2,3,5]; // first three primes (nice!)
var s := z[1,2,4]; // first three powers of 2 (tra-la-la)
var some: A;
f[i,j,k] := some;
call M3(i-1, j, k);
assert s == z[1,2,4];
if (*) {
assert f[i,j,k] == some; // error: the recursive call may have modified any element in 'f'
}
}
}
method M4(a: array2<bool>) returns (k: int)
requires a != null;
ensures 0 <= k;
{
k := a.Length0 + a.Length1;
}
}
|
