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
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
|
function G(int) returns (int);
axiom (forall x: int :: { G(x) } 0 <= x ==> G(x) == x);
function F(int) returns (int);
axiom (forall x: int :: { F(G(x)) } 0 <= x ==> F(G(x)) == 5);
procedure Lemma(y: int)
requires 0 <= y;
ensures F(y) == 5;
{
// proof:
assert G(y) == y;
}
procedure Main0()
{
assert F(2) == 5; // error: cannot prove this directly, because of the trigger
}
procedure Main1()
{
call Lemma(2);
assert F(2) == 5;
}
procedure Main2()
{
call Lemma(3);
assert F(2) == 5; // error: Lemma was instantiated the wrong way
}
procedure Main3()
{
call forall Lemma(*);
assert F(2) == 5;
}
procedure Main4()
{
call forall Lemma(*);
assert false; // error
}
procedure Main5(z: int)
{
call forall Lemma(*);
assert F(z) == 5; // error: z might be negative
}
procedure Main6(z: int)
requires 0 <= z;
{
call forall Lemma(*);
assert F(z) == 5;
}
// ------------ several parameters
function K(int, int) returns (int);
axiom (forall x: int, y: int :: { K(G(x), G(y)) } 0 <= x && 0 <= y ==> K(G(x), G(y)) == 25);
procedure MultivarLemma(x: int, y: int)
requires 0 <= x;
requires 0 <= y;
ensures K(x,y) == 25;
{
// proof:
assert G(x) == x;
assert G(y) == y;
}
procedure Multi0(x: int, y: int)
requires 0 <= x && 0 <= y;
{
assert K(x,y) == 25; // error
}
procedure Multi1(x: int, y: int)
requires 0 <= x && 0 <= y;
{
call MultivarLemma(x, y);
assert K(x,y) == 25;
}
procedure Multi2(x: int, y: int)
requires 0 <= x && 0 <= y;
{
call forall MultivarLemma(x, y);
assert K(x,y) == 25;
}
procedure Multi3(x: int, y: int)
requires 0 <= x && 0 <= y;
{
call forall MultivarLemma(*, y);
assert K(x,y) == 25;
}
procedure Multi4(x: int, y: int)
requires 0 <= x && 0 <= y;
{
call forall MultivarLemma(x, *);
assert K(x,y) == 25;
}
procedure Multi5(x: int, y: int)
requires 0 <= x && 0 <= y;
{
call forall MultivarLemma(2 + 100, *);
assert K(102, y) == 25;
assert false; // error
}
procedure Multi6(x: int, y: int)
requires 0 <= x && 0 <= y;
{
call forall MultivarLemma(*, y);
assert K(x+2,y+2) == 25; // error
}
procedure Multi7(x: int, y: int)
requires 0 <= x && 0 <= y;
{
call forall MultivarLemma(x, *);
assert K(x+2,y+2) == 25; // error
}
procedure Multi8(x: int, y: int)
requires 0 <= x && 0 <= y;
{
call forall MultivarLemma(*, *);
assert K(x+2,y+2) == 25; // that's the ticket!
}
|
