1 files changed, 115 insertions, 0 deletions
diff --git a/Chalice/refinements/Duplicates.chalice b/Chalice/refinements/Duplicates.chalice
new file mode 100644
index 00000000..52cdc3c3
--- /dev/null
+++ b/Chalice/refinements/Duplicates.chalice
@@ -0,0 +1,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;        
+      }
+    }
+  }
+}