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
144
145
146
147
148
149
150
151
|
// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
trait Automobile {
ghost var Repr: set<object>
predicate Valid()
reads this, Repr
ensures Valid() ==> this in Repr
function method Brand(): string
var position: int
method Drive()
requires Valid()
modifies Repr
ensures Valid() && fresh(Repr - old(Repr))
ensures old(position) <= position
}
class Fiat extends Automobile {
predicate Valid()
reads this, Repr
ensures Valid() ==> this in Repr
{
this in Repr && null !in Repr && position <= 100
}
constructor (pos: int)
requires pos <= 100
modifies this
ensures Valid() && fresh(Repr - {this}) && position == pos
{
position, Repr := pos, {this};
}
function method Brand(): string {
"Fiat"
}
method Drive()
requires Valid()
modifies Repr
ensures Valid() && fresh(Repr - old(Repr))
ensures old(position) <= position
{
position := if position < 97 then position + 3 else 100;
}
}
class Volvo extends Automobile {
var odometer: Odometer
predicate Valid()
reads this, Repr
ensures Valid() ==> this in Repr
{
this in Repr && null !in Repr && odometer in Repr &&
position % 10 == 0 && // position is always a multiple of 10
odometer.value == position
}
constructor ()
modifies this
ensures Valid() && fresh(Repr - {this})
{
position, Repr := 0, {this};
odometer := new Odometer();
Repr := Repr + {odometer};
}
function method Brand(): string {
"Volvo"
}
method Drive()
requires Valid()
modifies Repr
ensures Valid() && fresh(Repr - old(Repr))
ensures old(position) < position // always promises to make a move
{
position := position + 10;
odometer.Advance(10);
}
}
class Odometer {
var value: int
constructor ()
modifies this
ensures value == 0
{
value := 0;
}
method Advance(d: int)
requires 0 <= d
modifies this
ensures value == old(value) + d
{
value := value + d;
}
}
class Catacar extends Automobile {
var f: Fiat
var v: Volvo
predicate Valid()
reads this, Repr
ensures Valid() ==> this in Repr
{
this in Repr && null !in Repr &&
f in Repr && this !in f.Repr && f.Repr <= Repr && f.Valid() &&
v in Repr && this !in v.Repr && v.Repr <= Repr && v.Valid() &&
f.Repr !! v.Repr &&
position == f.position + v.position
}
constructor ()
modifies this
ensures Valid() && fresh(Repr - {this})
{
Repr := {this};
f := new Fiat(0); Repr := Repr + f.Repr;
v := new Volvo(); Repr := Repr + v.Repr;
position := v.position;
}
function method Brand(): string {
"Catacar"
}
method Drive()
requires Valid()
modifies Repr
ensures Valid() && fresh(Repr - old(Repr))
ensures old(position) <= position
{
f := new Fiat(f.position);
f.Drive(); v.Drive();
Repr := Repr + v.Repr + f.Repr;
position := f.position + v.position;
}
}
method Main() {
var auto: Automobile;
auto := new Fiat(0);
WorkIt(auto);
auto := new Volvo();
WorkIt(auto);
auto := new Catacar();
WorkIt(auto);
}
method WorkIt(auto: Automobile)
requires auto != null && auto.Valid()
modifies auto.Repr
{
auto.Drive();
auto.Drive();
assert old(auto.position) <= auto.position;
print auto.Brand(), ": ", auto.position, "\n";
auto.position := 18; // note, this may destroy the automobile's consistency condition (given by Valid)
}
|
