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".

4 files changed, 44 insertions, 17 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index be41fbf8..4edec058 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -91,8 +91,10 @@ TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the
 TypeTests.dfy(90,9): Error: sorry, cannot instantiate type parameter with a subrange type

 TypeTests.dfy(91,8): Error: sorry, cannot instantiate 'array' type with a subrange type

 TypeTests.dfy(92,8): Error: sorry, cannot instantiate 'array' type with a subrange type

+TypeTests.dfy(116,4): Error: cannot assign to non-ghost variable in a ghost context

+TypeTests.dfy(117,7): Error: cannot assign to non-ghost variable in a ghost context

 TypeTests.dfy(18,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed

-34 resolution/type errors detected in TypeTests.dfy

+36 resolution/type errors detected in TypeTests.dfy

 

 -------------------- NatTypes.dfy --------------------

 NatTypes.dfy(7,5): Error: value assigned to a nat must be non-negative

@@ -280,7 +282,7 @@ Execution trace:
     (0,0): anon37_Then

     (0,0): anon22

     (0,0): anon38_Then

-SmallTests.dfy(584,18): Error: target object may be null

+SmallTests.dfy(584,25): Error: target object may be null

 Execution trace:

     (0,0): anon0

 SmallTests.dfy(597,10): Error: assertion violation

@@ -1715,7 +1717,7 @@ Execution trace:
     (0,0): anon37_Then

     (0,0): anon22

     (0,0): anon38_Then

-SmallTests.dfy(584,18): Error: target object may be null

+SmallTests.dfy(584,25): Error: target object may be null

 Execution trace:

     (0,0): anon0

 SmallTests.dfy(597,10): Error: assertion violation

@@ -1863,7 +1865,7 @@ Execution trace:
     (0,0): anon37_Then

     (0,0): anon22

     (0,0): anon38_Then

-out.tmp.dfy(530,18): Error: target object may be null

+out.tmp.dfy(530,25): Error: target object may be null

 Execution trace:

     (0,0): anon0

 out.tmp.dfy(543,10): Error: assertion violation

diff --git a/Test/dafny0/ParallelResolveErrors.dfy b/Test/dafny0/ParallelResolveErrors.dfy
index ab711d02..f260edb5 100644
--- a/Test/dafny0/ParallelResolveErrors.dfy
+++ b/Test/dafny0/ParallelResolveErrors.dfy
@@ -103,6 +103,6 @@ method M1() {
 method M2() {

   var a := new int[100];

   parallel (x | 0 <= x < 100) {

-    a[x] :| a[x] > 0;  // error: not allowed to update heap location in a parallel statement with a(n implicit) assume

+    a[x] :| assume a[x] > 0;  // error: not allowed to update heap location in a parallel statement with an assume

   }

 }

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

 }

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 29274381..8434f06c 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -92,3 +92,28 @@ method K(s: set<nat>) {  // error: not allowed to instantiate 'set' with 'nat'
   var b := new nat[100,200];  // error: not allowed the type array2<nat>

 }

 

+// --------------------- more ghost tests, for assign-such-that statements

+

+method M()

+{

+  ghost var b: bool;

+  ghost var k: int, l: int;

+  var m: int;

+

+  // These three statements are allowed by the resolver, but the compiler will complain

+  // if it ever gets them.

+  k :| k < 10;

+  k, m :| 0 <= k < m;

+  m :| m < 10;

+

+  // Because of the ghost guard, these 'if' statements are ghost contexts, so only

+  // assignments to ghosts are allowed.

+  if (b) {

+    k :| k < 10;  // should be allowed

+    k, l :| 0 <= k < l;  // ditto

+  }

+  if (b) {

+    m :| m < 10;  // error: not allowed in ghost context

+    k, m :| 0 <= k < m;  // error: not allowed in ghost context

+  }

+}