Dafny: added assign-such-that statements; syntax: x,y,a[i],o.f :| Expr;

2 files changed, 188 insertions, 3 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 9995c817..22c24816 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -247,8 +247,47 @@ SmallTests.dfy(408,10): Error BP5003: A postcondition might not hold on this ret
 SmallTests.dfy(411,41): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon6_Else

+SmallTests.dfy(561,12): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Then

+    (0,0): anon2

+SmallTests.dfy(575,20): Error: left-hand sides 0 and 1 may refer to the same location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon27_Then

+    (0,0): anon28_Then

+    (0,0): anon4

+    (0,0): anon29_Then

+    (0,0): anon30_Then

+    (0,0): anon9

+    (0,0): anon31_Then

+    (0,0): anon32_Then

+    (0,0): anon12

+SmallTests.dfy(577,15): Error: left-hand sides 1 and 2 may refer to the same location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon27_Then

+    SmallTests.dfy(570,18): anon28_Else

+    (0,0): anon4

+    (0,0): anon29_Else

+    (0,0): anon7

+    (0,0): anon30_Then

+    (0,0): anon9

+    (0,0): anon31_Else

+    (0,0): anon35_Then

+    (0,0): anon36_Then

+    (0,0): anon37_Then

+    (0,0): anon22

+    (0,0): anon38_Then

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

+Execution trace:

+    (0,0): anon0

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

+Execution trace:

+    (0,0): anon0

 

-Dafny program verifier finished with 58 verified, 21 errors

+Dafny program verifier finished with 68 verified, 26 errors

 

 -------------------- Definedness.dfy --------------------

 Definedness.dfy(8,7): Error: possible division by zero

@@ -1598,8 +1637,47 @@ SmallTests.dfy(408,10): Error BP5003: A postcondition might not hold on this ret
 SmallTests.dfy(411,41): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon6_Else

+SmallTests.dfy(561,12): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Then

+    (0,0): anon2

+SmallTests.dfy(575,20): Error: left-hand sides 0 and 1 may refer to the same location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon27_Then

+    (0,0): anon28_Then

+    (0,0): anon4

+    (0,0): anon29_Then

+    (0,0): anon30_Then

+    (0,0): anon9

+    (0,0): anon31_Then

+    (0,0): anon32_Then

+    (0,0): anon12

+SmallTests.dfy(577,15): Error: left-hand sides 1 and 2 may refer to the same location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon27_Then

+    SmallTests.dfy(570,18): anon28_Else

+    (0,0): anon4

+    (0,0): anon29_Else

+    (0,0): anon7

+    (0,0): anon30_Then

+    (0,0): anon9

+    (0,0): anon31_Else

+    (0,0): anon35_Then

+    (0,0): anon36_Then

+    (0,0): anon37_Then

+    (0,0): anon22

+    (0,0): anon38_Then

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

+Execution trace:

+    (0,0): anon0

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

+Execution trace:

+    (0,0): anon0

 

-Dafny program verifier finished with 58 verified, 21 errors

+Dafny program verifier finished with 68 verified, 26 errors

 out.tmp.dfy(33,11): Error: index out of range

 Execution trace:

     (0,0): anon0

@@ -1707,8 +1785,47 @@ out.tmp.dfy(469,10): Error BP5003: A postcondition might not hold on this return
 out.tmp.dfy(470,41): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon6_Else

+out.tmp.dfy(507,12): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Then

+    (0,0): anon2

+out.tmp.dfy(521,20): Error: left-hand sides 0 and 1 may refer to the same location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon27_Then

+    (0,0): anon28_Then

+    (0,0): anon4

+    (0,0): anon29_Then

+    (0,0): anon30_Then

+    (0,0): anon9

+    (0,0): anon31_Then

+    (0,0): anon32_Then

+    (0,0): anon12

+out.tmp.dfy(523,15): Error: left-hand sides 1 and 2 may refer to the same location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon27_Then

+    out.tmp.dfy(516,18): anon28_Else

+    (0,0): anon4

+    (0,0): anon29_Else

+    (0,0): anon7

+    (0,0): anon30_Then

+    (0,0): anon9

+    (0,0): anon31_Else

+    (0,0): anon35_Then

+    (0,0): anon36_Then

+    (0,0): anon37_Then

+    (0,0): anon22

+    (0,0): anon38_Then

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

+Execution trace:

+    (0,0): anon0

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

+Execution trace:

+    (0,0): anon0

 

-Dafny program verifier finished with 58 verified, 21 errors

+Dafny program verifier finished with 68 verified, 26 errors

 

 -------------------- LetExpr.dfy --------------------

 LetExpr.dfy(5,12): Error: assertion violation

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 914e228e..4d219cd3 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -535,3 +535,71 @@ static method TestNotNot()
 

   assert true == !(!true);

 }

+

+// ----------------------- Assign-such-that statements -------

+

+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;

+  } else {

+    var xx, yy :| 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;'

+  assert b < a;

+  k :| 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;

+  assert 3 !in T;

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

+}

+

+method AssignSuchThat2(i: int, j: int, ghost S: set<Node>)

+  modifies S;

+{

+  var n := new Node;

+  var a := new int[25];

+  var t;

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

+    a[i], t, a[j], n.next, n :| 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)

+  } 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])

+  }

+}

+

+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)

+}

+

+method AssignSuchThat4()

+{

+  var n := new Node;

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

+}

+

+method AssignSuchThat5()

+{

+  var n := new Node;

+  n :| 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;'

+  assert false;  // no problemo

+}