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
|
// 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))
}
// 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) ) { // error: cannot compile this guard of a non-ghost if statement
h := 6;
}
}
****/
}
|
