Chalice:

* added celebrity example (theory of sequences is still weak to prove basic things...)
* bug in Chalice: old in while loops is ignored, needs to be fixed if ever want to complete DSW example
* evil input from Z3 makes subsequent refinement proofs unsound; need to debug before building upon DSW.chalice; the error is triggered when adding parent field to Node

3 files changed, 63 insertions, 112 deletions

diff --git a/Chalice/refinements/Celebrity.chalice b/Chalice/refinements/Celebrity.chalice
new file mode 100644
index 00000000..b0d398e0
--- /dev/null
+++ b/Chalice/refinements/Celebrity.chalice
@@ -0,0 +1,48 @@
+// Celebrity example, inspired by the Rodin tutorial

+class Person {

+  function knows(other: Person): bool

+    requires this != other;

+}

+

+class Celebrity0 {

+  function IsCelebrity(c: Person, people: seq<Person>): bool

+    requires null !in people;

+  {

+    c in people && forall p in people :: p != c ==> (p.knows(c)) && (! c.knows(p))

+  }

+

+  method Find(people: seq<Person>, /*ghost*/ c: Person) returns (r: Person)

+    requires null !in people && IsCelebrity(c, people);

+  {

+    var r [r == c];

+  }

+}

+

+/** Without theory of sets, hard to describe: "remove an element from a sequence" */

+class Celebrity1 refines Celebrity0 {

+  refines Find(people: seq<Person>, c: Person) returns (r: Person)

+  {

+    var q:seq<Person> := people;

+

+    // pick and remove a

+    var a:Person := q[0]; q := q[1..]; assert people == [a] ++ q;

+      

+    while (|q| > 0)   

+      invariant forall p in q :: p in people;

+      invariant a in people;

+      invariant IsCelebrity(c,[a] ++ q);  

+    {      

+      // pick and remove b

+      var oldq:seq<Person> := q;

+      var b:Person := q[0]; q := q[1..]; 

+      assert oldq == [b] ++ q;

+

+      if (a != b && a.knows(b)) {

+        a := b;

+      }      

+    }         

+

+    r := a;

+  }

+}

+

diff --git a/Chalice/refinements/DSW.chalice b/Chalice/refinements/DSW.chalice
index 78a84354..5be52f96 100644
--- a/Chalice/refinements/DSW.chalice
+++ b/Chalice/refinements/DSW.chalice
@@ -5,8 +5,6 @@ class Node {
   var children: seq<Node>;
   var marked: bool;
   ghost var path: seq<Node>;
-
-  var parent: Node;
 }
 
 class DSW0 {
@@ -58,13 +56,7 @@ class DSW0 {
       // termination
       invariant stop ==> |stack| == 0 && (forall ch in t.children :: ch.marked);
     {
-      var n: Node;
-
-      // stupid syntactic trick to make transformers go around call
-      if (true) {
-        call n := PickUnmarked(t.children); 
-      }
-
+      call n := PickUnmarked(t.children); 
       if (n != null) {
         // push             
         stack := [t] ++ stack;          
@@ -95,43 +87,17 @@ class DSW0 {
   }
 }
 
-class DSW1 refines DSW0 {
-  transforms IterativeMark(root: Node, S: seq<Node>) 
-  {
-    assume forall n in S :: n.parent == null;
-    _
-    while 
-      invariant forall n in S :: n !in stack ==> n.parent == null;
-      invariant forall i in [1..|stack|] :: stack[i-1].parent == stack[i];
-    {
-      _
-      if {*}
-      if {
-        // push
-        if (|stack| > 0) {
-          t.parent := stack[0];
-        }
-        *
-      } else {
-        // pop
-        if {*} else {
-          _
-          t.parent := null;
-        }
-      }
-    }
-  }
-
-  transforms PickUnmarked(p: seq<Node>) returns (x: Node)
-  {
-    replaces x by {
-      if (|p| == 0) {
-        x := null;
-      } else if (! p[0].marked) {
-        x := p[0];
-      } else {
-        call x := PickUnmarked(p[1..]);
-      }
-    }
-  }
-}
\ No newline at end of file
+class DSW1 refines DSW0 {

+  transforms PickUnmarked(p: seq<Node>) returns (x: Node)

+  {

+    replaces x by {

+      if (|p| == 0) {

+        x := null;

+      } else if (! p[0].marked) {

+        x := p[0];

+      } else {

+        call x := PickUnmarked(p[1..]);

+      }

+    }

+  }

+}
diff --git a/Chalice/refinements/original/Celebrity.chalice b/Chalice/refinements/original/Celebrity.chalice
deleted file mode 100644
index 266ebb1b..00000000
--- a/Chalice/refinements/original/Celebrity.chalice
+++ /dev/null
@@ -1,63 +0,0 @@
-// Celebrity example, inspired by the Rodin tutorial

-class Person {

-  var knows: seq<Person>;

-}

-

-class Celebrity {

-  function IsCelebrity(c: Person, people: seq<Person>): bool

-    requires forall p in people :: p != null;

-    requires c in people && rd(people[*].knows);

-  {

-    forall p in people :: p != c ==> (c in p.knows) && (p !in c.knows)

-  }

-

-  method FindCelebrity0(people: seq<Person>) returns (r: Person)

-    requires null !in people && rd(people[*].knows); 

-    requires exists c in people :: IsCelebrity(c, people);

-    ensures rd(people[*].knows);

-    ensures r in people && IsCelebrity(r, people);

-  {

-    var cc:Person; 

-    assume cc in people && IsCelebrity(cc, people);

-    r := cc;

-  }

-

-  method FindCelebrity1(people: seq<Person>) returns (r: Person)

-    requires null !in people && rd(people[*].knows);

-    requires exists c in people :: IsCelebrity(c, people);

-    ensures rd(people[*].knows);

-    ensures r in people && IsCelebrity(r, people);

-  {

-    call r := Eliminate0(people, people);

-  }

-  

-  method Eliminate0(Q: seq<Person>, people: seq<Person>) returns (r: Person)

-    requires null !in people && rd(people[*].knows);

-    requires forall c in Q :: c != null && c in people;

-    requires exists c in Q :: IsCelebrity(c, people);  

-    ensures rd(people[*].knows);

-    ensures r in people && IsCelebrity(r, people);

-  {

-    if (|Q| == 1) {

-      r := Q[0];

-    } else {

-      var x:Person := Q[0];

-      var y:Person := Q[1];

-      var W:seq<Person>;

-      assume x != y;

-      if (y in x.knows) {

-        W := Q[1..];

-        assert !IsCelebrity(x, people);          

-        assert Q == [x] ++ W; 

-      } else {

-        W := [x] ++ Q[2..];

-        assert !IsCelebrity(y, people);

-        assert W[0] == x;

-        assert W[1..] == Q[2..];

-

-        assert exists c in W :: IsCelebrity(c, people);

-      }

-      call r := Eliminate0(W, people);

-    }

-  }

-}