blob: 52cdc3c314fec53e061d69cfaaffba066fd56091 (
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
|
class Duplicates0 {
// 3. we can do fast set checks if we know the bounds on the elements
method find(s: seq<int>) returns (b:bool)
requires forall i in s :: 0 <= i && i < 100;
{
var b [b == (exists i in [0..|s|] :: s[i] in s[..i]) ];
}
}
class Duplicates1 refines Duplicates0 {
refines find(s: seq<int>) returns (b: bool)
{
b := false;
// 0. need a loop
// 1. need a set data structure
var i := 0;
var d := new Set0;
call d.init();
// 6. use a witness from the loop
ghost var w;
while (i < |s|)
invariant 0 <= i && i <= |s|;
// 5. add loop invariants using value of Set.add: equivalence as a set
invariant acc(d.rep);
// 6. assert equivalent as sets of d.rep and s[..i]
invariant forall n in d.rep :: n in s[..i];
invariant forall n in [0..i] :: s[n] in d.rep;
// 7. devise termination conditions to satisfy the spec
invariant b ==> 0 <= w && w < |s| && s[w] in s[..w];
invariant !b ==> (forall j,k in [0..i] :: j != k ==> s[j] != s[k]);
{
call r := d.add(s[i]);
assert r ==> d.rep[0] == s[i]; // help out sequence axioms
if (! r) {
b := true;
w := i;
}
i := i + 1;
}
}
}
class Set0 {
var rep: seq<int>;
method init()
requires acc(rep);
ensures acc(rep) && |rep| == 0;
{
rep := nil<int>;
}
method add(i) returns (b:bool)
requires acc(rep);
requires 0 <= i && i < 100;
ensures acc(rep);
ensures (i in old(rep)) ==> !b && rep == old(rep);
ensures (i !in old(rep)) ==> b && rep == [i] ++ old(rep);
{
// 2. need a way to compute whether element is in the set
var c:bool [c <==> i in old(rep)];
if (c) {
b := false;
} else {
b := true;
rep := [i] ++ rep;
assert rep[0] == i;
}
}
}
class Set1 refines Set0 {
var bitset: seq<bool>;
// 4. represent a set as a bitset (provided representation invariant of the uppermost class)
replaces rep by acc(bitset) &&
/** representation invariant */ (forall i in rep :: 0 <= i && i < 100) && |bitset| == 100 &&
/** coupling invariant */ (forall j in [0..100] :: bitset[j] <==> (j in rep))
refines init()
{
var i := 0;
bitset := nil<bool>;
while (i < 100)
invariant i <= 100 && acc(bitset);
invariant |bitset| == i;
invariant forall b in bitset :: ! b;
{
bitset := [false] ++ bitset;
i := i + 1;
}
}
transforms add(i) returns (b: bool)
{
replaces c by {var c:bool := this.bitset[i]}
if {
*
} else {
replaces * by {
b := true;
var s:seq<bool> := [true] ++ this.bitset[i+1..];
assert s[0] == true; // help out sequence axioms
s := this.bitset[..i] ++ s;
this.bitset := s;
}
}
}
}
|
