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
143
|
module M0 {
datatype Kind = Constant | Ident | Binary;
class Expr {
var kind: Kind;
var value: int; // value if kind==Constant; id if kind==VarDecl; operator if kind==Binary
var left: Expr; // if kind==Binary
var right: Expr; // if kind==Binary
ghost var Repr: set<object>;
predicate Valid()
reads this, Repr;
{
this in Repr && null !in Repr &&
(left != null ==> left in Repr && this !in left.Repr && right !in left.Repr && left.Repr <= Repr && left.Valid()) &&
(right != null ==> right in Repr && this !in right.Repr && left !in right.Repr && right.Repr <= Repr && right.Valid()) &&
(kind == Binary ==> left != null && right != null && left.Repr !! right.Repr)
}
constructor CreateConstant(x: int)
modifies this;
ensures Valid() && fresh(Repr - {this});
{
kind, value := Constant, x;
left, right := null, null;
Repr := {this};
}
constructor CreateIdent(name: int)
modifies this;
ensures Valid() && fresh(Repr - {this});
{
kind, value := Ident, name;
left, right := null, null;
Repr := {this};
}
constructor CreateBinary(op: int, left: Expr, right: Expr)
requires left != null && left.Valid() && this !in left.Repr;
requires right != null && right.Valid() && this !in right.Repr;
requires left.Repr !! right.Repr;
modifies this;
ensures Valid() && fresh(Repr - {this} - left.Repr - right.Repr);
{
kind, value := Binary, op;
this.left, this.right := left, right;
Repr := {this} + left.Repr + right.Repr;
}
}
}
// Introduce the idea of resolved
module M1 refines M0 {
class Expr {
ghost var resolved: bool;
predicate Valid()
{
resolved ==>
(kind == Binary ==> left.resolved && right.resolved)
}
constructor CreateConstant...
{
resolved := false;
}
constructor CreateIdent...
{
resolved := false;
}
constructor CreateBinary...
{
resolved := false;
}
method Resolve()
requires Valid(); // it's okay if it's already resolved
modifies Repr;
ensures Valid() && fresh(Repr - old(Repr));
ensures resolved;
decreases Repr;
{
if (kind == Binary) {
left.Resolve();
right.Resolve();
}
Repr := Repr + (if left != null then left.Repr else {}) + (if right != null then right.Repr else {});
resolved := true;
}
}
}
// Give "resolved" some meaning
module M2 refines M1 {
class VarDecl {
}
class Expr {
var decl: VarDecl; // if kind==Ident, filled in during resolution
predicate Valid()
{
resolved ==>
(kind == Ident ==> decl != null)
}
method Resolve...
{
if (kind == Ident) {
decl := new VarDecl;
}
}
}
}
// Finally, supposing each VarDecl has a value, evaluate a resolved expression
module M3 refines M2 {
class VarDecl {
var val: int;
}
class Expr {
method Eval() returns (r: int)
requires Valid();
requires resolved;
decreases Repr;
{
match (kind) {
case Constant =>
r := value;
case Ident =>
r := decl.val; // note how this statement relies on "decl" being non-null, which follows from the expression being resolved
case Binary =>
var x := left.Eval();
var y := right.Eval();
r := x + y;
}
}
}
}
|
