blob: abb2a4293ead71cc3769aea5a97a83182e53930e (
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
|
class Duplicates0 {
method find(s:seq<int>) returns (b: bool)
requires forall i in s :: i in [0..100];
{
spec b [b <==> exists i in [0..|s|] :: s[i] in s[..i] ];
}
}
class Duplicates1 refines Duplicates0 {
refines find(s:seq<int>) returns (b: bool)
{
var n := 0;
b := false;
while (n < |s|)
invariant 0 <= n && n <= |s|;
invariant b <==> exists i in [0..n] :: s[i] in s[..i];
{
spec c:bool [c <==> s[n] in s[..n] ];
b := b || c;
n := n + 1;
}
}
}
class Dupllcates2 refines Duplicates1 {
transforms find(s: seq<int>) returns (b: bool)
{
_;
var bitset:seq<bool> [|bitset| == 100 && true !in bitset ];
while
invariant |bitset| == 100;
invariant forall i in [0..n] :: bitset[ s[i] ];
invariant forall j in [0..100] :: bitset[j] ==> j in s[..n];
{
replaces c by {
var c: bool := bitset[ s[n] ];
}
bitset := bitset[..s[n] ] ++ [true] ++ bitset[ s[n] + 1 ..];
_
}
}
}
|