Chalice:

* fix bugs -- translateAssert and etran.fromPreGlobals were referring to globals by name instead of using current globals
* example of finding duplicate elements in a sequence using a bitset

2 files changed, 119 insertions, 5 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;        

+      }

+    }

+  }

+}

diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index 2ab7f668..3b6955b1 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -414,9 +414,9 @@ class Translator {
         val tmpTranslator = new ExpressionTranslator(List(tmpHeap._1.id, tmpMask._1.id, tmpCredits._1.id), List(etran.ChooseEtran(true).Heap, etran.ChooseEtran(true).Mask, etran.ChooseEtran(true).Credits), currentClass);        

         Comment("assert") ::

         // exhale e in a copy of the heap/mask/credits

-        BLocal(tmpHeap._1) :: (tmpHeap._2 := VarExpr(HeapName)) ::

-        BLocal(tmpMask._1) :: (tmpMask._2 := VarExpr(MaskName)) ::

-        BLocal(tmpCredits._1) :: (tmpCredits._2 := VarExpr(CreditsName)) ::

+        BLocal(tmpHeap._1) :: (tmpHeap._2 := etran.Heap) ::

+        BLocal(tmpMask._1) :: (tmpMask._2 := etran.Mask) ::

+        BLocal(tmpCredits._1) :: (tmpCredits._2 := etran.Credits) ::

         tmpTranslator.Exhale(List((e, ErrorMessage(s.pos, "Assertion might not hold."))), "assert", true)

       case Assume(e) =>

         Comment("assume") ::

@@ -1363,9 +1363,8 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
   }

 

   def FromPreGlobals(preGlobals: List[Boogie.BVar]) = {

-    val g = for ((id,t) <- ExpressionTranslator.Globals) yield VarExpr(id)

     val pg = preGlobals map (g => new VarExpr(g))

-    new ExpressionTranslator(g, pg, currentClass, checkTermination)

+    new ExpressionTranslator(globals, pg, currentClass, checkTermination)

   }

 

   def UseCurrentAsOld() = {