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
|
// 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 {
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 // error: reads is not self-framing (unless "this in Repr")
requires this in Repr // lo and behold! So, reads clause is fine, if we can assume the precondition
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)
}
|
