blob: d73f8373e82292cbb6e5fce3d2bf0b630d6b0e5c (
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
|
class Char {}
class StringBuilder0 {
var rep: seq<Char>;
method Init()
requires acc(rep);
ensures acc(rep);
{ rep := nil<Char>; }
function ToString(): seq<Char>
requires rd(rep);
{ rep }
method Append(chars: seq<Char>)
requires acc(rep);
ensures acc(rep);
ensures ToString() == old(ToString()) ++ chars;
{ rep := rep ++ chars; }
}
class Chunk0 {
var rep: seq<Char>;
ghost var start;
}
class StringBuilder1 refines StringBuilder0 {
var chunks: seq<Chunk0>;
replaces rep by acc(chunks) && acc(chunks[*].rep) && acc(chunks[*].start) &&
/** representation invariant */ null !in chunks && |chunks| > 0 &&
chunks[0].start == 0 &&
(forall i in [0..|chunks|-1] :: chunks[i+1].start == chunks[i].start + |chunks[i].rep|) &&
/** coupling invariant */ (forall c in chunks :: c.rep == rep[c.start..c.start + |c.rep|])
refines Init()
{
var c := new Chunk0;
c.rep := nil<Char>;
c.start := 0;
chunks := [c];
rep := nil<Char>;
}
refines Append(chars: seq<Char>)
{
rep := rep ++ chars;
var i; assume 0 <= i && i < |chars|;
if (i > 0) {
call AppendChunk(chunks[|chunks|-1], chars[..i]);
}
if (i < |chars| - 1) {
call ExpandByABlock();
call AppendChunk(chunks[|chunks|-1], chars[i..]);
}
}
method AppendChunk(ch: Chunk0, chars: seq<Char>)
{
ch.rep := ch.rep ++ chars;
}
method ExpandByABlock()
{
var c := new Chunk0;
c.rep := nil<Char>;
chunks := chunks ++ [c];
}
}
|
