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
|
type T;
const zero: T;
function IsProperIndex(i: int, size: int): bool;
procedure P(a: [int]T, n: int)
requires (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
{
call Q(a, n);
}
procedure Q(a: [int]T, n: int)
requires (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
{
call P(a, n);
}
procedure A(a: [int]T, n: int)
{
assert
(forall i : int :: IsProperIndex(i, n) ==> a[i] == zero)
==>
(forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
}
procedure B(a: [int]T, n: int)
{
assert
(forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|)
==>
(forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
}
procedure C(a: [int]T, n: int)
{
Start:
assume (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
goto Next;
Next:
assert (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
}
procedure D(a: [int]T, n: int)
{
Start:
assume (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
goto Next;
Next:
assert (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
}
|
