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
|
// RUN: %dafny /compile:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// Checking that the reads clause also is checked over requires
class C { var u : int; }
function nope1(c : C):()
requires c != null && c.u > 0;
{()}
function ok1(c : C):()
requires c != null && c.u > 0;
reads c;
{()}
function nope2(c : C):()
requires c != null && c.u > 0;
reads if c != null then {} else {c};
{()}
function ok2(c : C):()
requires c != null && c.u > 0;
reads if c != null then {c} else {};
{()}
function nope3(xs : seq<C>):()
requires |xs| > 0 && xs[0] != null && xs[0].u > 0;
{()}
function ok3(xs : seq<C>):()
requires |xs| > 0 && xs[0] != null && xs[0].u > 0;
reads xs;
{()}
function nope4(c : C, xs : set<C>):()
requires c != null && c !in xs ==> c.u > 0;
reads xs;
{()}
function ok4(c : C, xs : set<C>):()
requires c != null && c in xs ==> c.u > 0;
reads xs;
{()}
// reads over itself
class R { var r : R; }
function nope5(r : R):()
reads if r != null then {r.r} else {};
{()}
function ok5(r : R):()
reads if r != null then {r, r.r} else {};
{()}
// Reads checking where there are circularities among the expressions
class CircularChecking {
ghost var Repr: set<object>
function F(): int
reads this, Repr
function F'(): int
reads Repr, this // this is also fine
function G0(): int
reads this
requires Repr == {} && F() == 100
function G1(): int
reads this
requires F() == 100 // fine, since the next line tells us that Repr is empty
requires Repr == {}
function H0(cell: Cell): int
reads Repr // by itself, this reads is not self-framing
requires this in Repr // lo and behold! So, reads clause is fine after all
function H1(cell: Cell): int
reads this, Repr
requires cell in Repr
requires cell != null && cell.data == 10
function H2(cell: Cell): int
reads this, Repr
requires cell != null && cell.data == 10 // this is okay, too, since reads checks are postponed
requires cell in Repr
}
class Cell { var data: int }
// Test the benefits of the new reads checking for function checking
function ApplyToSet<X>(S: set<X>, f: X -> X): set<X>
requires forall x :: x in S ==> f.reads(x) == {} && f.requires(x)
{
if S == {} then {} else
var x :| x in S;
ApplyToSet(S - {x}, f) + {f(x)}
}
function ApplyToSet_AltSignature0<X>(S: set<X>, f: X -> X): set<X>
requires forall x :: x in S ==> f.requires(x) && f.reads(x) == {}
function ApplyToSet_AltSignature1<X>(S: set<X>, f: X -> X): set<X>
requires forall x :: x in S ==> f.reads(x) == {}
requires forall x :: x in S ==> f.requires(x)
function ApplyToSet_AltSignature2<X>(S: set<X>, f: X -> X): set<X>
requires (forall x :: x in S ==> f.reads(x) == {}) ==> forall x :: x in S ==> f.requires(x)
// (this precondition would not be good enough to check the body above)
function FunctionInQuantifier0(): int
requires exists f: int -> int :: f(10) == 100 // error (x2): precondition violation and insufficient reads
function FunctionInQuantifier1(): int
requires exists f: int -> int :: f.requires(10) && f(10) == 100 // error: insufficient reads
function FunctionInQuantifier2(): int
requires exists f: int -> int :: f.reads(10) == {} && f.requires(10) && f(10) == 100
ensures FunctionInQuantifier2() == 100
{
var f: int -> int :| f.reads(10) == {} && f.requires(10) && f(10) == 100; // fine :) :)
f(10)
}
class DynamicFramesIdiom {
ghost var Repr: set<object>
predicate IllFormed_Valid()
reads Repr // error: reads is not self framing (notice the absence of "this")
{
this in Repr // this says that the predicate returns true if "this in Repr", but the
// predicate can also be invoked in a state where its body will evaluate to false
}
}
|
