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
|
// 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) // error: MyReadsBad does not have permission to read what f.reads(a) reads
}
function MyReadsBad2(f : A -> B, a : A) : set<object>
{
(f.reads)(a) // error: MyReadsBad2 does not have permission to read what f.reads(a) reads
}
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) // error: MyReadsBad' does not have permission to read what f.reads(a) reads
}
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) // error: MyRequiresBad does not have permission to read what f.requires(a) reads
}
}
module WhatWeKnowAboutReads {
function ReadsNothing():(){()}
lemma IndeedNothing() {
assert ReadsNothing.reads() == {};
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) == {}; // error
} else if * { assert s' !in ReadsSomething.reads(s);
} else if * { assert s' in ReadsSomething.reads(s); // error
}
}
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) == {}; // error
} else if * { assert s' !in f.reads(s);
} else if * { assert s' in f.reads(s); // error
}
}
}
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)
}
}
module ReadsOnFunctions {
lemma Requires_Reads_What_Function_Reads(f: int -> int)
{
var g := f.requires;
assert g.reads(10) == f.reads(10);
}
}
|
