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
|
// Trigger errors
function f(int, int) returns (int);
function P(int, int) returns (bool);
axiom (forall x: int ::
{ f(x,10) && f(x,9) } // error: && not allowed
f(x,10) == 3);
axiom (forall x: int ::
{ ((((f(x,10) || f(x,9))))) } // error: || not allowed
f(x,10) == 3);
axiom (forall x: int ::
{ !f(x,10) } // error: ! not allowed
f(x,10) == 3);
axiom (forall x: int ::
{ (!f(x,10)) } // error: ! not allowed
f(x,10) == 3);
axiom (forall x: int ::
{ P(x,10) ==> P(20,x) } // error: ==> not allowed
f(x,10) == 3);
axiom (forall x: int ::
{ P(x,10) <==> P(20,x) } // error: <==> not allowed
f(x,10) == 3);
axiom (forall x: int ::
{ f(x,10) == 3 } // error: == not allowed
f(x,10) == 3);
axiom (forall x: int ::
{ f(x,10) < 3 } // error: < not allowed
f(x,10) == 3);
axiom (forall x: int ::
{ f(x,10) + f(x,x) != 3 } // yes, != is allowed
f(x,10) == 3);
axiom (forall b: bool ::
{ (forall y: int :: b) } // error: quantifiers not allowed
b);
// -------------- tests of free variables
const g: int;
axiom (forall x: int ::
{ false, 6 } // error: does not mention "x"
x < x + 1);
axiom (forall x: int ::
{ false, x+1, 6 } // allowed
x < x + 1);
axiom (forall x: int, y: int ::
{ x+1 } // error: does not mention "y"
{ y+1 } // error: does not mention "x"
x < y + 1);
axiom (forall x: int ::
{ g+x != 65 } // allowed
x < x + 1);
axiom (forall x: int ::
{ x } // "x" by itself is not a good trigger
x < x + 1);
//axiom (forall x: any :: // PR: removed for the time being
// { cast(x,int) } // can't fool me, still not allowed
// x == x );
// --- multiple triggers
axiom (forall x: int, y: int, z: int ::
{ x+y+z } // good
{ x+y, y+z } // also good
{ f(f(x,y),y) } // error: does not mention z
x == x );
// --- multi-triggers
axiom (forall x: int, y: int, z: int ::
{ f(x,x), f(y,y), f(z,z) } // good
f(x,y) < f(y,z) );
// --- pattern exclusion
axiom (forall x: int, y: int ::
{:nopats x } // error: "x" by itself is not allowed here either
{:nopats g } // error: "g" by itself is not allowed here either
x < y);
axiom (forall x: int, y: int ::
{:nopats f(g,g) } // but it is okay not to mention the bound variables (in a pattern exclusion)
x < y);
// --- merging of nested quantifiers
axiom (forall x:int :: (forall y:int :: { f(x,y) } f(x,y) > 0)); // OK
axiom (forall x:int :: (forall y:int :: { f(x,x) } f(x,x) > 0)); // error
axiom (forall x:int :: (forall y:int :: { f(y,y) } f(y,y) > 0)); // error
// three levels
axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,y) } f(y,y) > 0))); // error
axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,z) } f(y,y) > 0))); // error
axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(y,z) } f(y,y) > 0))); // error
axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,y), f(y,z) } f(y,y) > 0))); // OK
// --- no free variables
var h0: int;
var h1: [ref,ref]int;
axiom (forall o: ref, f: ref :: h1[o,f] // error: cannot mention free variable "h1"
< h0); // error: cannot mention free variable "h0"
const c0: int;
const c1: [ref,ref]int;
axiom (forall o: ref, f: ref :: c1[o,f] < c0);
type ref;
|
