Dafny:

* Fixed bug in translation of well-formedness conditions
* Added Test/dafny0/Celebrity.dfy
* Added a harness to Test/vacid0/Composite.dfy

7 files changed, 137 insertions, 4 deletions

diff --git a/Dafny/Translator.ssc b/Dafny/Translator.ssc
index eea9d91b..092ee146 100644
--- a/Dafny/Translator.ssc
+++ b/Dafny/Translator.ssc
@@ -1303,7 +1303,8 @@ namespace Microsoft.Dafny {
           substMap.Add(p, ie);

           locals.Add(new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.UniqueName, TrType(local.Type))));

           Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(ie);  // TODO: is this cast always justified?

-          Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, etran.TrExpr(e.Args[i]));

+          Expression ee = e.Args[i];

+          Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, etran.CondApplyBox(p.tok, etran.TrExpr(ee), (!)ee.Type, p.Type));

           builder.Add(cmd);

         }

         // check that the preconditions for the call hold

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 59582de8..e1b83c87 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -418,7 +418,7 @@ TypeParameters.dfy(63,27): Error: assertion violation
 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 20 verified, 2 errors

+Dafny program verifier finished with 24 verified, 2 errors

 

 -------------------- Datatypes.dfy --------------------

 

@@ -443,3 +443,7 @@ Dafny program verifier finished with 12 verified, 0 errors
 -------------------- Tree.dfy --------------------

 

 Dafny program verifier finished with 6 verified, 0 errors

+

+-------------------- Celebrity.dfy --------------------

+

+Dafny program verifier finished with 11 verified, 0 errors

diff --git a/Test/dafny0/Celebrity.dfy b/Test/dafny0/Celebrity.dfy
new file mode 100644
index 00000000..fd267c71
--- /dev/null
+++ b/Test/dafny0/Celebrity.dfy
@@ -0,0 +1,95 @@
+// Celebrity example, inspired by the Rodin tutorial

+

+method Pick<T>(S: set<T>) returns (t: T);

+  requires S != {};

+  ensures t in S;

+

+static function Knows<Person>(a: Person, b: Person): bool;

+  requires a != b;  // forbid asking about the reflexive case

+

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

+{

+  c in people &&

+  (forall p :: p in people && p != c ==> Knows(p, c) && !Knows(c, p))

+}

+

+method FindCelebrity0<Person>(people: set<Person>, ghost c: Person) returns (r: Person)

+  requires (exists c :: IsCelebrity(c, people));

+  ensures r == c;

+{

+  var cc; assume cc == c;  // this line essentially converts ghost c to non-ghost cc

+  r := cc;

+}

+

+method FindCelebrity1<Person>(people: set<Person>, ghost c: Person) returns (r: Person)

+  requires IsCelebrity(c, people);

+  ensures r == c;

+{

+  var Q := people;

+  call x := Pick(Q);

+  while (Q != {x})

+    //invariant Q <= people;  // inv1 in Rodin's Celebrity_1, but it's not needed here

+    invariant IsCelebrity(c, Q);  // inv2

+    invariant x in Q;

+    decreases Q;

+  {

+    call y := Pick(Q - {x});

+    if (Knows(x, y)) {

+      Q := Q - {x};  // remove_1

+    } else {

+      Q := Q - {y};  assert x in Q;  // remove_2

+    }

+    call x := Pick(Q);

+  }

+  r := x;

+}

+

+method FindCelebrity2<Person>(people: set<Person>, ghost c: Person) returns (r: Person)

+  requires IsCelebrity(c, people);

+  ensures r == c;

+{

+  call b := Pick(people);

+  var R := people - {b};

+  while (R != {})

+    invariant R <= people;  // inv1

+    invariant b in people;  // inv2

+    invariant b !in R;  // inv3

+    invariant IsCelebrity(c, R + {b});  // my non-refinement way of saying inv4

+

+    decreases R;

+  {

+    call x := Pick(R);

+    if (Knows(x, b)) {

+      R := R - {x};

+    } else {

+      b := x;

+      R := R - {x};

+    }

+  }

+  r := b;

+}

+

+method FindCelebrity3(n: int, people: set<int>, ghost c: int) returns (r: int)

+  requires 0 < n;

+  requires (forall p :: p in people <==> 0 <= p && p < n);

+  // requires IsCelebrity(c, people);  // see next line:

+  requires c in people && (forall p :: p in people && p != c ==> Knows(p, c) && !Knows(c, p));  // hack to work around bug in Dafny-to-Boogie translator

+  ensures r == c;

+{

+  r := 0;

+  var a := 1;

+  var b := 0;

+  while (a < n)

+    invariant a <= n;

+    invariant b < a;  // Celebrity_2/inv3 and Celebrity_3/inv2

+    invariant c == b || (a <= c && c < n);

+  {

+    if (Knows(a, b)) {

+      a := a + 1;

+    } else {

+      b := a;

+      a := a + 1;

+    }

+  }

+  r := b;

+}

diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy
index 614c2185..e199a386 100644
--- a/Test/dafny0/TypeParameters.dfy
+++ b/Test/dafny0/TypeParameters.dfy
@@ -96,3 +96,19 @@ class CClient {
     assert z == c.x;

   }

 }

+

+// -------------------------

+

+static function IsCelebrity<Person>(c: Person, people: set<Person>): bool;

+  requires c == c || c in people;

+

+method FindCelebrity3(people: set<int>, ghost c: int)

+  requires IsCelebrity(c, people);

+{

+  ghost var b: bool;

+  b := IsCelebrity(c, people);

+  b := F(c, people);

+}

+

+static function F(c: int, people: set<int>): bool;

+  requires IsCelebrity(c, people);

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index c43ea782..eb7ea4f7 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -23,7 +23,7 @@ for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy Array.dfy
             SchorrWaite.dfy Termination.dfy Use.dfy DTypes.dfy

             TypeParameters.dfy Datatypes.dfy UnboundedStack.dfy

             SumOfCubes.dfy TerminationDemos.dfy Substitution.dfy

-            Tree.dfy) do (

+            Tree.dfy Celebrity.dfy) do (

   echo.

   echo -------------------- %%f --------------------

   %DAFNY_EXE% /compile:0 %* %%f

diff --git a/Test/vacid0/Answer b/Test/vacid0/Answer
index 6f270f92..90bbcc78 100644
--- a/Test/vacid0/Answer
+++ b/Test/vacid0/Answer
@@ -9,4 +9,4 @@ Dafny program verifier finished with 9 verified, 0 errors
 

 -------------------- Composite.dfy --------------------

 

-Dafny program verifier finished with 14 verified, 0 errors

+Dafny program verifier finished with 16 verified, 0 errors

diff --git a/Test/vacid0/Composite.dfy b/Test/vacid0/Composite.dfy
index 28074c7b..ca5f206b 100644
--- a/Test/vacid0/Composite.dfy
+++ b/Test/vacid0/Composite.dfy
@@ -83,6 +83,7 @@ class Composite {
     ensures (forall c :: c in S ==> c.Valid(S));

     ensures (forall c :: c in S ==> c.val == old(c.val));

     ensures (forall c :: c in S && c != this ==> c.parent == old(c.parent));

+    ensures parent == null;

     ensures (forall c :: c in S ==> c.left == old(c.left) || (old(c.left) == this && c.left == null));

     ensures (forall c :: c in S ==> c.right == old(c.right) || (old(c.right) == this && c.right == null));

     ensures Acyclic({this});

@@ -158,3 +159,19 @@ method Main()
   call c2.Update(496, S);

   call c0.Update(0, S);

 }

+

+method Harness() {

+  var a := new Composite;  call a.Init(5);

+  var b := new Composite;  call b.Init(7);

+  call a.Add({a}, b, {b});

+  assert a.sum == 12;

+

+  call b.Update(17, {a,b});

+  assert a.sum == 22;

+

+  var c := new Composite;  call c.Init(10);

+  call b.Add({a,b}, c, {c});

+  call b.Dislodge({a,b,c});

+  assert b.sum == 27;

+}

+