Dafny: Changed the semantics of the assign-such-that statement "x :| P;" to check the existence of a value. The previous "assume only" version is available by supplying the keyword "assume" in front of "P".

1 files changed, 12 insertions, 12 deletions

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 4d219cd3..e8b618d7 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -542,21 +542,21 @@ method AssignSuchThat0(a: int, b: int) returns (x: int, y: int)
   ensures x == a && y == b;

 {

   if (*) {

-    x, y :| a <= x < a + 1 && b + a <= y + a && y <= b;

+    x, y :| assume a <= x < a + 1 && b + a <= y + a && y <= b;

   } else {

-    var xx, yy :| a <= xx < a + 1 && b + a <= yy + a && yy <= b;

+    var xx, yy :| assume a <= xx < a + 1 && b + a <= yy + a && yy <= b;

     x, y := xx, yy;

   }

 }

 

 method AssignSuchThat1(a: int, b: int) returns (x: int, y: int)

 {

-  var k :| 0 <= k < a - b;  // this acts like an 'assume 0 < a - b;'

+  var k :| assume 0 <= k < a - b;  // this acts like an 'assume 0 < a - b;'

   assert b < a;

-  k :| k == old(2*k);  // note, the 'old' has no effect on local variables like k

+  k :| assume k == old(2*k);  // note, the 'old' has no effect on local variables like k

   assert k == 0;

   var S := {2, 4, 7};

-  var T :| T <= S;

+  var T :| assume T <= S;

   assert 3 !in T;

   assert T == {};  // error: T may be larger

 }

@@ -568,38 +568,38 @@ method AssignSuchThat2(i: int, j: int, ghost S: set<Node>)
   var a := new int[25];

   var t;

   if (0 <= i < j < 25) {

-    a[i], t, a[j], n.next, n :| true;

+    a[i], t, a[j], n.next, n :| assume true;

   }

   if (n != null && n.next != null) {

     assume n in S && n.next in S;

-    n.next.next, n.next :| n != null && n.next != null && n.next.next == n.next;  // error: n.next may equal n (thus aliasing n.next.next and n.next)

+    n.next.next, n.next :| assume n != null && n.next != null && n.next.next == n.next;  // error: n.next may equal n (thus aliasing n.next.next and n.next)

   } else if (0 <= i < 25 && 0 <= j < 25) {

-    t, a[i], a[j] :| t < a[i] < a[j];  // error: i may equal j (thus aliasing a[i] and a[j])

+    t, a[i], a[j] :| assume t < a[i] < a[j];  // error: i may equal j (thus aliasing a[i] and a[j])

   }

 }

 

 method AssignSuchThat3()

 {

   var n := new Node;

-  n, n.next :| n.next == n;  // error: RHS is not well defined (RHS is evaluated after the havocking of the LHS)

+  n, n.next :| assume n.next == n;  // error: RHS is not well defined (RHS is evaluated after the havocking of the LHS)

 }

 

 method AssignSuchThat4()

 {

   var n := new Node;

-  n, n.next :| n != null && n.next == n;  // that's the ticket

+  n, n.next :| assume n != null && n.next == n;  // that's the ticket

 }

 

 method AssignSuchThat5()

 {

   var n := new Node;

-  n :| fresh(n);  // fine

+  n :| assume fresh(n);  // fine

   assert false;  // error

 }

 

 method AssignSuchThat6()

 {

   var n: Node;

-  n :| n != null && fresh(n);  // there is no non-null fresh object, so this amounts to 'assume false;'

+  n :| assume n != null && fresh(n);  // there is no non-null fresh object, so this amounts to 'assume false;'

   assert false;  // no problemo

 }