blob: 5f084bd45b684cb3ff06316e76a91f5a4f507495 (
plain)
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
|
// RUN: %dafny /print:"%t.print" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
class Ref<A> {
var val: A;
}
method Nope() {
var f : Ref<int -> bool>;
var g : int -> bool;
f := new Ref<int -> bool>;
f.val := x => true;
g := x reads f reads f.val.reads(x) => !f.val(x);
}
method M() {
var f : Ref<int -> bool>;
var g : int -> bool;
f := new Ref<int -> bool>;
f.val := x => true;
g := x reads f reads f.val.reads(x) requires f.val.requires(x) => !f.val(x);
f.val := g;
if (!g(0)) {
assert !g(0);
} else {
assert g(0);
}
}
method L() {
var f : Ref<() -> bool>;
f := new Ref<() -> bool>;
f.val := () reads f reads f.val.reads() requires !f.val.requires() => true;
if (f.val.requires()) {
assert !f.val.requires();
} else {
assert f.val.requires();
}
}
method LRead() {
var o : object;
var f : Ref<() -> bool>;
f := new Ref<() -> bool>;
f.val := () reads f
reads f.val.reads()
reads if o in f.val.reads() then {} else {o}
=> true;
assume o != null;
assert o != f;
if (o in f.val.reads()) {
assert o !in f.val.reads();
} else {
assert o in f.val.reads();
}
}
|
