blob: 3886cb7891e2db8c1aedda4158c75dc20c6a53e5 (
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
|
class Duplicates0 {
method Find(s: seq<int>) returns (b: bool)
requires forall i in s :: i in [0..100];
{
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];
{
var c := s[n] in s[..n];
b := b || c;
n := n + 1;
}
}
}
class Duplicates2 refines Duplicates1 {
transforms Find(s: seq<int>) returns (b: bool)
{
_;
// bitset has length 100, initially all false
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 ..];
_;
}
}
}
|
