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
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
|
method M0(n: int)
requires var f := 100; n < f; requires var t, f := true, false; (t && f) || n < 100;
{
assert n < 200;
assert 0 <= n; // error
}
method M1()
{
assert var f := 54; var g := f + 1; g == 55;
}
method M2()
{
assert var f := 54; var f := f + 1; f == 55;
}
function method Fib(n: nat): nat
{
if n < 2 then n else Fib(n-1) + Fib(n-2)
}
method M3(a: array<int>) returns (r: int)
requires a != null && forall i :: 0 <= i < a.Length ==> a[i] == 6;
ensures (r + var t := r; t*2) == 3*r;
{
assert Fib(2) + Fib(4) == Fib(0) + Fib(1) + Fib(2) + Fib(3);
{
var x,y := Fib(8), Fib(11);
assume x == 21;
assert Fib(7) == 3 ==> Fib(9) == 24;
assume Fib(1000) == 1000;
assume Fib(9) - Fib(8) == 13;
assert Fib(9) <= Fib(10);
assert y == 89;
}
assert Fib(1000) == 1000; // does it still know this?
parallel (i | 0 <= i < a.Length) ensures true; {
var j := i+1;
assert j < a.Length ==> a[i] == a[j];
}
}
// M4 is pretty much the same as M3, except with things rolled into expressions.
method M4(a: array<int>) returns (r: int)
requires a != null && forall i :: 0 <= i < a.Length ==> a[i] == 6;
ensures (r + var t := r; t*2) == 3*r;
{
assert Fib(2) + Fib(4) == Fib(0) + Fib(1) + Fib(2) + Fib(3);
assert
var x,y := Fib(8), Fib(11);
assume x == 21;
assert Fib(7) == 3 ==> Fib(9) == 24;
assume Fib(1000) == 1000;
assume Fib(9) - Fib(8) == 13;
assert Fib(9) <= Fib(10);
y == 89;
assert Fib(1000) == 1000; // still known, because the assume was on the path here
assert forall i :: 0 <= i < a.Length ==> var j := i+1; j < a.Length ==> a[i] == a[j];
}
var index: int;
method P(a: array<int>) returns (b: bool, ii: int)
requires a != null && exists k :: 0 <= k < a.Length && a[k] == 19;
modifies this, a;
ensures ii == index;
// The following uses a variable with a non-old definition inside an old expression:
ensures 0 <= index < a.Length && old(a[ii]) == 19;
ensures 0 <= index < a.Length && var newIndex := index; old(a[newIndex]) == 19;
// The following places both the variable and the body inside an old:
ensures b ==> old(var oldIndex := index; 0 <= oldIndex < a.Length && a[oldIndex] == 17);
// Here, the definition of the variable is old, and it's used both inside and
// inside an old expression:
ensures var oi := old(index); oi == index ==> a[oi] == 21 && old(a[oi]) == 19;
{
b := 0 <= index < a.Length && a[index] == 17;
var i, j := 0, -1;
while (i < a.Length)
invariant 0 <= i <= a.Length;
invariant forall k :: 0 <= k < i ==> a[k] == 21;
invariant forall k :: i <= k < a.Length ==> a[k] == old(a[k]);
invariant (0 <= j < i && old(a[j]) == 19) ||
(j == -1 && exists k :: i <= k < a.Length && a[k] == 19);
{
if (a[i] == 19) { j := i; }
i, a[i] := i + 1, 21;
}
index := j;
ii := index;
}
method PMain(a: array<int>)
requires a != null && exists k :: 0 <= k < a.Length && a[k] == 19;
modifies this, a;
{
var s := a[..];
var b17, ii := P(a);
assert s == old(a[..]);
assert s[index] == 19;
if (*) {
assert a[index] == 19; // error (a can have changed in P)
} else {
assert b17 ==> 0 <= old(index) < a.Length && old(a[index]) == 17;
assert index == old(index) ==> a[index] == 21 && old(a[index]) == 19;
}
}
|
