blob: 6c4c12ad499616e26f2cdf5ab9fb64670b9d2542 (
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
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 /print:"%t.print" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
class C { var u : int; }
method M(f : int -> int)
requires f.requires(0);
{
var init := f(0);
var o := new C;
assert init == f(0);
}
method M2()
{
var c := new C;
c.u := 0;
var f := () reads c => c.u;
var init := f();
c.u := 1;
if * {
assert f() == init; // should fail
} else {
assert f() == 1;
}
}
method M3()
{
var c := new C;
c.u := 0;
var f := () reads c => c.u;
assert f() == 0;
c.u := 1;
assert f() == 1;
assert f() == 0; // should fail
assert false; // should fail
}
method Main() {
var x := 2;
var getX := () => x;
assert getX() == 2;
x := 3;
assert getX() == 2; // the value is copied
}
method Refs() {
var a := new int[1];
a[0] := 2;
var get;
if * {
get := () reads a => a[0]; // OK
assert get() == 2;
a[0] := 3;
assert get() == 3; // OK, the ref is copied, but not the entire array
a := new int[0];
assert get() == 3; // OK, still 3
assert get() == 0 || get() == 2; // fail: is three!
} else if * {
get := () => a[0]; // fail: Not enough read
} else {
get := () reads {} => a[0]; // fail: Not enough read
}
}
method Fiddling(k : int -> int)
{
var mkGet := (arr : array<int>) =>
() reads arr requires arr != null requires arr.Length > 0 => arr[0];
var a := new int[1];
var b := new int[1];
var get := mkGet(a);
a[0] := 0;
b[0] := 10;
assert get() == a[0];
b[0] := 20;
assert get() == a[0];
}
method HeapSucc0(k : int -> int)
requires k.requires(0);
{
var init := k(0);
var a := new object;
assert k(0) == init;
}
method HeapSucc1(k : int -> int, c : C)
requires k.requires(0);
requires c !in k.reads(0);
modifies c;
{
var init := k(0);
if ( c != null ) {
c.u := c.u + 1;
assert k(0) == init;
}
}
method HeapSucc2(k : int -> int, c : C)
requires k.requires(0);
modifies c;
{
var init := k(0);
if ( c != null ) {
c.u := c.u + 1;
if ( c !in k.reads(0) ) {
assert k(0) == init;
} else {
assert k(0) == init; // Fail
}
}
}
|
