Translate let-such-that expressions

3 files changed, 111 insertions, 4 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 13e7a8b0..85d8c977 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -277,8 +277,26 @@ Execution trace:
 SmallTests.dfy(576,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

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

+Execution trace:

+    (0,0): anon0

+    (0,0): anon8_Then

+    (0,0): anon9_Then

+    (0,0): anon4

+    (0,0): anon10_Then

+    (0,0): anon7

+SmallTests.dfy(618,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Then

+    (0,0): anon6_Then

+    (0,0): anon3

+SmallTests.dfy(620,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Else

 

-Dafny program verifier finished with 70 verified, 26 errors

+Dafny program verifier finished with 75 verified, 29 errors

 

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

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

@@ -554,7 +572,12 @@ ResolutionErrors.dfy(377,10): Error: second argument to ==> must be of type bool
 ResolutionErrors.dfy(382,6): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

 ResolutionErrors.dfy(434,7): Error: ghost variables are allowed only in specification contexts

 ResolutionErrors.dfy(440,12): Error: ghost variables are allowed only in specification contexts

-68 resolution/type errors detected in ResolutionErrors.dfy

+ResolutionErrors.dfy(508,7): Error: let-such-that expressions are allowed only in ghost contexts

+ResolutionErrors.dfy(510,7): Error: let-such-that expressions are allowed only in ghost contexts

+ResolutionErrors.dfy(510,20): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(512,7): Error: let-such-that expressions are allowed only in ghost contexts

+ResolutionErrors.dfy(513,18): Error: unresolved identifier: w

+73 resolution/type errors detected in ResolutionErrors.dfy

 

 -------------------- ParseErrors.dfy --------------------

 ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator

@@ -2048,8 +2071,26 @@ Execution trace:
 SmallTests.dfy(576,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

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

+Execution trace:

+    (0,0): anon0

+    (0,0): anon8_Then

+    (0,0): anon9_Then

+    (0,0): anon4

+    (0,0): anon10_Then

+    (0,0): anon7

+SmallTests.dfy(618,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Then

+    (0,0): anon6_Then

+    (0,0): anon3

+SmallTests.dfy(620,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Else

 

-Dafny program verifier finished with 70 verified, 26 errors

+Dafny program verifier finished with 75 verified, 29 errors

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

 Execution trace:

     (0,0): anon0

@@ -2193,8 +2234,26 @@ Execution trace:
 out.tmp.dfy(522,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

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

+Execution trace:

+    (0,0): anon0

+    (0,0): anon8_Then

+    (0,0): anon9_Then

+    (0,0): anon4

+    (0,0): anon10_Then

+    (0,0): anon7

+out.tmp.dfy(563,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Then

+    (0,0): anon6_Then

+    (0,0): anon3

+out.tmp.dfy(565,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Else

 

-Dafny program verifier finished with 70 verified, 26 errors

+Dafny program verifier finished with 75 verified, 29 errors

 

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

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

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index bcd1a077..69b8ea38 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -499,3 +499,17 @@ module NoTypeArgs1 {
     t

   }

 }

+

+// ----------- let-such-that expressions ------------------------

+

+method LetSuchThat(ghost z: int, n: nat)

+{

+  var x: int;

+  x := var y :| y < 0; y;  // fine

+

+  x := var y :| y < z; y;  // error (x2): RHS depends on a ghost (both on the :| expression and on the z variable)

+

+  x := var w :| w == 2*w; w;

+  x := var w := 2*w; w;  // error: the 'w' in the RHS of the assignment is not in scope

+  ghost var xg := var w :| w == 2*w; w;

+}

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 43ee1d8e..c55d6140 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -587,3 +587,37 @@ method AssignSuchThat7<T>(A: set<T>, x: T) {
   var B :| A <= B;

   assert x in A ==> x in B;

 }

+

+// ----------- let-such-that expressions ------------------------

+

+function method LetSuchThat_P(x: int): bool

+

+method LetSuchThat0(ghost g: int)

+  requires LetSuchThat_P(g);

+{

+  var t :| LetSuchThat_P(t);  // assign-such-that statement

+  ghost var u := var q :| LetSuchThat_P(q); q + 1;  // let-such-that expression

+  if (forall a,b | LetSuchThat_P(a) && LetSuchThat_P(b) :: a == b) {

+    assert t < u;

+  }

+  assert LetSuchThat_P(u-1);  // yes

+  assert LetSuchThat_P(u);  // error: no reason to expect this to hold

+}

+

+method LetSuchThat1<T>(A: set<T>)

+{

+  ghost var C := var B :| A <= B; A - B;

+  assert C == {};

+}

+

+method LetSuchThat2(n: nat)

+{

+  ghost var x := (var k :| k < n; k) + 3;  // fine, such a k always exists

+  assert x < n+3;

+  if (*) {

+    x := var k :| 0 <= k < n; k;  // error: there may not be such a k

+  } else {

+    x := var k: nat :| k < n; k;  // error: there may not be such a k

+  }

+}

+