blob: b5ecfbfa359813679df529422988e704b4d56ed2 (
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
|
// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
abstract module M0 {
class Cell {
var data: int;
constructor (d: int)
modifies this;
ensures data == d;
{ data := d; }
}
class Counter {
ghost var N: int;
ghost var Repr: set<object>;
protected predicate Valid()
reads this, Repr;
{
this in Repr
}
constructor Init()
modifies this;
ensures N == 0;
ensures Valid() && fresh(Repr - {this});
{
Repr := {};
ghost var repr :| {this} <= repr && fresh(repr - {this});
N, Repr := 0, repr;
}
method Inc()
requires Valid();
modifies Repr;
ensures N == old(N) + 1;
ensures Valid() && fresh(Repr - old(Repr));
{
N := N + 1;
modify Repr - {this};
}
method Get() returns (n: int)
requires Valid();
ensures n == N;
{
n :| assume n == N;
}
}
}
module M1 refines M0 {
class Counter {
var c: Cell;
var d: Cell;
protected predicate Valid...
{
c != null && c in Repr &&
d != null && d in Repr &&
c != d &&
N == c.data - d.data
}
constructor Init...
{
c := new Cell(0);
d := new Cell(0);
...;
ghost var repr := Repr + {this} + {c,d};
}
method Inc...
{
...;
modify ... {
c.data := c.data + 1;
}
}
method Get...
{
n := c.data - d.data;
}
}
}
|