Chalice/refinements/DuplicatesVideo.chalice


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 ..];
      _
    }
  }
}