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
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
|
// This file contains various tests of resolving quantifiers in ghost and non-ghost positions
class MyClass<T> {
// This function is in a ghost context, so all is cool.
function GhostF(): bool
{
(forall n :: 2 <= n ==> (exists d :: n < d && d < 2*n))
}
// But try to make it a non-ghost function, and Dafny will object because it cannot compile the
// body into code that will terminate.
function method NonGhostF(): bool
{
(forall n :: 2 <= n ==> (exists d :: n < d && d < 2*n)) // error: can't figure out how to compile
}
// Add an upper bound to n and things are cool again.
function method NonGhostF_Bounded(): bool
{
(forall n :: 2 <= n && n < 1000 ==> (exists d :: n < d && d < 2*n))
}
// Although the heuristics applied are syntactic, they do see through the structure of the boolean
// operators ==>, &&, ||, and !. Hence, the following three variations of the previous function can
// also be compiled.
function method NonGhostF_Or(): bool
{
(forall n :: !(2 <= n && n < 1000) || (exists d :: n < d && d < 2*n))
}
function method NonGhostF_ImpliesImplies(): bool
{
(forall n :: 2 <= n ==> n < 1000 ==> (exists d :: n < d && d < 2*n))
}
function method NonGhostF_Shunting(): bool
{
(forall n :: 2 <= n ==> 1000 <= n || (exists d :: n < d && d < 2*n))
}
function method GoodRange(): bool
{
(forall n | 2 <= n :: 1000 <= n || (exists d | n < d :: d < 2*n)) && (exists K: nat | K < 100 :: true)
}
function method BadRangeForall(): bool
{
forall n | n <= 2 :: 1000 <= n || n % 2 == 0 // error: cannot bound range for n
}
function method BadRangeExists(): bool
{
exists d | d < 1000 :: d < 2000 // error: cannot bound range for d
}
function method WhatAboutThis(): bool
{
forall n :: 2 <= n && (forall M | M == 1000 :: n < M) ==> n % 2 == 0 // error: heuristics don't get this one for n
}
// Here are more tests
function method F(a: array<T>): bool
requires a != null;
reads a;
{
(exists i :: 0 <= i && i < a.Length / 2 && (forall j :: i <= j && j < a.Length ==> a[i] == a[j]))
}
function method G0(a: seq<T>): bool
{
(exists t :: t in a && (forall u :: u in a ==> u == t))
}
function method G1(a: seq<T>): bool
{
(exists ti :: 0 <= ti && ti < |a| && (forall ui :: 0 <= ui && ui < |a| ==> a[ui] == a[ti]))
}
// Regrettably, the heuristics don't know about transitivity:
function method IsSorted0(s: seq<int>): bool
{
(forall i, j :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]) // error: can't figure out how to compile
}
function method IsSorted1(s: seq<int>): bool
{
(forall j, i :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]) // error: can't figure out how to compile
}
// Add the redundant conjunct "i < |s|" and things are fine.
function method IsSorted2(s: seq<int>): bool
{
(forall i, j :: 0 <= i && i < |s| && i < j && j < |s| ==> s[i] <= s[j])
}
// But if you switch the order of i and j, you need a different redundant conjunct.
function method IsSorted3(s: seq<int>): bool
{
(forall j, i :: 0 <= i && i < |s| && i < j && j < |s| ==> s[i] <= s[j]) // error: can't figure out how to compile
}
function method IsSorted4(s: seq<int>): bool
{
(forall j, i :: 0 <= i && 0 < j && i < j && j < |s| ==> s[i] <= s[j])
}
// The heuristics look at bound variables in the order given, as is illustrated by the following
// two functions.
function method Order0(S: seq<set<int>>): bool
{
(forall i, j :: 0 <= i && i < |S| && j in S[i] ==> 0 <= j)
}
function method Order1(S: seq<set<int>>): bool
{
(forall j, i :: 0 <= i && i < |S| && j in S[i] ==> 0 <= j) // error: can't figure out how to compile
}
// Quantifiers can be used in other contexts, too.
// For example, in assert statements and assignment statements.
method M(s: seq<int>) returns (r: bool, q: bool) {
assert (forall x :: x in s ==> 0 <= x);
r := (forall x :: x in s ==> x < 100);
q := (exists y :: y*y in s); // error: can't figure out how to compile
}
// And if expressions.
function method Select_Good(S: set<int>, a: T, b: T): T
{
if (forall x :: x in S ==> 0 <= x && x < 100) then a else b
}
function method Select_Bad(S: set<int>, a: T, b: T): T
{
if (forall x :: x*x in S ==> 0 <= x && x < 100) then a else b // error: can't figure out how to compile
}
// (the same thing, but in a ghost function is fine, though)
function Select_Bad_Ghost(S: set<int>, a: T, b: T): T
{
if (forall x :: x*x in S ==> 0 <= x && x < 100) then a else b
}
// And if statements
method N(s: seq<int>) returns (ghost g: int, h: int)
{
if ( (forall x :: x in s ==> 0 <= x) ) {
h := 0; g := 0;
}
if ( (forall x :: x*x in s ==> x < 100) ) { // this is fine, since the whole statement is a ghost statement
g := 2;
}
if ( (forall x :: x*x in s ==> x < 50) ) {
h := 6; // error: cannot compile this guard of a non-ghost if statement
}
}
}
// The following functions test what was once a soundness problem
module DependencyOnAllAllocatedObjects {
function AllObjects0(): bool
{
forall c: SomeClass :: c != null ==> c.f == 0 // error: not allowed to dependend on which objects are allocated
}
function AllObjects1(): bool
{
forall c: SomeClass :: true // error: not allowed to dependend on which objects are allocated
}
function AllObjects10(): bool
reads *;
{
forall c: SomeClass :: c != null ==> c.f == 0 // error: not allowed to dependend on which objects are allocated
}
function AllObjects11(): bool
reads *;
{
forall c: SomeClass :: true // error: not allowed to dependend on which objects are allocated
}
function method AllObjects20(): bool
{
forall c: SomeClass :: c != null ==> c.f == 0 // error: not allowed to dependend on which objects are allocated
}
function method AllObjects21(): bool
{
forall c: SomeClass :: true // error: not allowed to dependend on which objects are allocated
}
function method AllObjects30(): bool
reads *;
{
forall c: SomeClass :: c != null ==> c.f == 0 // error: not allowed to dependend on which objects are allocated
}
function method AllObjects31(): bool
reads *;
{
forall c: SomeClass :: true // error: not allowed to dependend on which objects are allocated
}
method M()
{
var b := forall c: SomeClass :: c != null ==> c.f == 0; // error: non-ghost code requires bounds
ghost var g := forall c: SomeClass :: c != null ==> c.f == 0; // cool (this is in a ghost context
// outside a function)
}
class SomeClass {
var f: int;
}
}
|
