blob: 03aef62d73289d191e7803345bcde5ebe1121411 (
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
129
130
131
132
133
134
135
136
137
138
139
140
141
|
// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// give the method signatures and specs
abstract module M0 {
class {:autocontracts} Container<T(==)> {
ghost var Contents: set<T>;
protected predicate Valid()
constructor ()
ensures Contents == {};
method Add(t: T)
ensures Contents == old(Contents) + {t};
method Remove(t: T)
ensures Contents == old(Contents) - {t};
method Contains(t: T) returns (b: bool)
ensures Contents == old(Contents);
ensures b <==> t in Contents;
}
}
// provide bodies for the methods
abstract module M1 refines M0 {
class Container<T(==)> {
constructor... {
Contents := {};
}
method Add... {
Contents := Contents + {t};
}
method Remove... {
Contents := Contents - {t};
}
method Contains... {
// b := t in Contents;
b :| assume b <==> t in Contents;
}
}
}
// implement the set in terms of a sequence
module M2 refines M1 {
class Container<T(==)> {
var elems: seq<T>;
protected predicate Valid()
{
Contents == (set x | x in elems) &&
forall i,j :: 0 <= i < j < |elems| ==> elems[i] != elems[j]
}
method FindIndex(t: T) returns (j: nat)
ensures j <= |elems|;
ensures if j < |elems| then elems[j] == t else t !in elems;
{
j := 0;
while (j < |elems|)
invariant j <= |elems|;
invariant forall i :: 0 <= i < j ==> elems[i] != t;
{
if (elems[j] == t) {
return;
}
j := j + 1;
}
}
constructor... {
elems := [];
}
method Add... {
var j := FindIndex(t);
if (j == |elems|) {
elems := elems + [t];
}
}
method Remove... {
var j := FindIndex(t);
if (j < |elems|) {
elems := elems[..j] + elems[j+1..];
}
}
method Contains... {
var j := FindIndex(t);
b := j < |elems|;
}
}
}
// implement a cache
module M3 refines M2 {
class Container<T(==)> {
var cachedValue: T;
var cachedIndex: int;
protected predicate Valid() {
0 <= cachedIndex ==> cachedIndex < |elems| && elems[cachedIndex] == cachedValue
}
constructor... {
cachedIndex := -1;
}
method FindIndex... {
if (0 <= cachedIndex && cachedValue == t) {
return cachedIndex;
}
}
method Remove... {
...;
if ... {
if (cachedIndex == j) {
// clear the cache
cachedIndex := -1;
} else if (j < cachedIndex) {
// adjust for the shifting down
cachedIndex := cachedIndex - 1;
}
}
}
}
}
// here a client of the Container
module Client {
import M as M0 default M2
method Test() {
var c := new M.Container();
c.Add(56);
c.Add(12);
var b := c.Contains(17);
assert !b;
b := c.Contains(12);
assert b;
c.Remove(12);
b := c.Contains(12);
assert !b;
assert c.Contents == {56};
}
}
module CachedClient refines Client {
import M = M3
method Main() {
Test();
}
}
|
