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
|
// 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);
}
}
}
module ReadsAll {
function A(f: int -> int) : int
reads set o,x | o in f.reads(x) :: o;
requires forall x :: f.requires(x);
{
f(0) + f(1) + f(2)
}
function method B(f: int -> int) : int
reads set o,x | o in f.reads(x) :: o;
requires forall x :: f.requires(x);
{
f(0) + f(1) + f(2)
}
function C(f: int -> int) : int
reads f.reads;
requires forall x :: f.requires(x);
{
f(0) + f(1) + f(2)
}
function method D(f: int -> int) : int
reads f.reads;
requires forall x :: f.requires(x);
{
f(0) + f(1) + f(2)
}
}
|
