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
|
class Node {
var next: Node;
function IsList(r: set<Node>): bool
reads r;
{
this in r &&
(next != null ==> next.IsList(r - {this}))
}
method Test(n: Node, nodes: set<Node>)
{
assume nodes == nodes - {n};
// the next line needs the Set extensionality axiom, the antecedent of
// which is supplied by the previous line
assert IsList(nodes) == IsList(nodes - {n});
}
method Create()
modifies this;
{
next := null;
var tmp: Node;
tmp := new Node;
assert tmp != this; // was once a bug in the Dafny checker
}
method SequenceUpdateOutOfBounds(s: seq<set<int>>, j: int) returns (t: seq<set<int>>)
{
t := s[j := {}]; // error: j is possibly out of bounds
}
method Sequence(s: seq<bool>, j: int, b: bool, c: bool) returns (t: seq<bool>)
requires 10 <= |s|;
requires 8 <= j && j < |s|;
ensures |t| == |s|;
ensures t[8] == s[8] || t[9] == s[9];
ensures t[j] == b;
{
if (c) {
t := s[j := b];
} else {
t := s[..j] + [b] + s[j+1..];
}
}
method Max0(x: int, y: int) returns (r: int)
ensures r == (if x < y then y else x);
{
if (x < y) { r := y; } else { r := x; }
}
method Max1(x: int, y: int) returns (r: int)
ensures r == x || r == y;
ensures x <= r && y <= r;
{
r := if x < y then y else x;
}
function PoorlyDefined(x: int): int
requires if next == null then 5/x < 20 else true; // error: ill-defined then branch
requires if next == null then true else 0 <= 5/x; // error: ill-defined then branch
requires if next.next == null then true else true; // error: ill-defined guard
requires 10/x != 8; // this is well-defined, because we get here only if x is non-0
reads this;
{
12
}
}
// ------------------ modifies clause tests ------------------------
class Modifies {
var x: int;
var next: Modifies;
method A(p: Modifies)
modifies this, p;
{
x := x + 1;
while (p != null && p.x < 75)
decreases 75 - p.x; // error: not defined at top of each iteration (there's good reason to
{ // insist on this; for example, the decrement check could not be performed
p.x := p.x + 1; // at the end of the loop body if p were set to null in the loop body)
}
}
method B(p: Modifies)
modifies this;
{
call A(this);
if (p == this) {
call p.A(p);
}
call A(p); // error: may violate modifies clause
}
method C(b: bool)
modifies this;
ensures !b ==> x == old(x) && next == old(next);
{
}
method D(p: Modifies, y: int)
requires p != null;
{
if (y == 3) {
call p.C(true); // error: may violate modifies clause
} else {
call p.C(false); // error: may violation modifies clause (the check is done without regard
// for the postcondition, which also makes sense, since there may, in
// principle, be other fields of the object that are not constrained by the
// postcondition)
}
}
method E()
modifies this;
{
call A(null); // allowed
}
method F(s: set<Modifies>)
modifies s;
{
foreach (m in s | 2 <= m.x) {
m.x := m.x + 1;
}
if (this in s) {
x := 2 * x;
}
}
method G(s: set<Modifies>)
modifies this;
{
var m := 3; // this is a different m
foreach (m in s | m == this) {
m.x := m.x + 1;
}
if (s <= {this}) {
foreach (m in s) {
m.x := m.x + 1;
}
call F(s);
}
foreach (m in s) {
assert m.x < m.x + 10; // nothing wrong with asserting something
m.x := m.x + 1; // error: may violate modifies clause
}
}
}
|
