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
|
// RUN: %dafny /print:"%t.print" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
module ReadsRequiresReads {
function MyReadsOk(f : A -> B, a : A) : set<object>
reads f.reads(a);
{
f.reads(a)
}
function MyReadsOk2(f : A -> B, a : A) : set<object>
reads f.reads(a);
{
(f.reads)(a)
}
function MyReadsOk3(f : A -> B, a : A) : set<object>
reads (f.reads)(a);
{
f.reads(a)
}
function MyReadsOk4(f : A -> B, a : A) : set<object>
reads (f.reads)(a);
{
(f.reads)(a)
}
function MyReadsBad(f : A -> B, a : A) : set<object>
{
f.reads(a)
}
function MyReadsBad2(f : A -> B, a : A) : set<object>
{
(f.reads)(a)
}
function MyReadsOk'(f : A -> B, a : A, o : object) : bool
reads f.reads(a);
{
o in f.reads(a)
}
function MyReadsBad'(f : A -> B, a : A, o : object) : bool
{
o in f.reads(a)
}
function MyRequiresOk(f : A -> B, a : A) : bool
reads f.reads(a);
{
f.requires(a)
}
function MyRequiresBad(f : A -> B, a : A) : bool
{
f.requires(a)
}
}
module WhatWeKnowAboutReads {
function ReadsNothing():(){()}
lemma IndeedNothing() {
assert ReadsNothing.reads() == {};
}
method NothingHere() {
assert (() => ()).reads() == {};
}
class S {
var s : S;
}
function ReadsSomething(s : S):()
reads s;
{()}
method MaybeSomething() {
var s := new S;
var s' := new S;
if * { assert s in ReadsSomething.reads(s) || ReadsSomething.reads(s) == {};
} else if * { assert s in ReadsSomething.reads(s);
} else if * { assert ReadsSomething.reads(s) == {};
} else if * { assert s' !in ReadsSomething.reads(s);
} else if * { assert s' in ReadsSomething.reads(s);
}
}
method SomethingHere() {
var s := new S;
var s' := new S;
var f := (u) reads u => ();
if * { assert s in f.reads(s) || f.reads(s) == {};
} else if * { assert s in f.reads(s);
} else if * { assert f.reads(s) == {};
} else if * { assert s' !in f.reads(s);
} else if * { assert s' in f.reads(s);
}
}
}
|
