improved and fixed compilation and resolution of assign-such-that statements

5 files changed, 36 insertions, 11 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 370e3c38..e7fda470 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -91,10 +91,11 @@ TypeTests.dfy(90,6): Error: sorry, cannot instantiate collection type with a sub
 TypeTests.dfy(91,9): Error: sorry, cannot instantiate type parameter with a subrange type

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

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

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

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

+TypeTests.dfy(105,15): Error: ghost variables are allowed only in specification contexts

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

+TypeTests.dfy(116,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

-36 resolution/type errors detected in TypeTests.dfy

+37 resolution/type errors detected in TypeTests.dfy

 

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

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

@@ -556,7 +557,9 @@ ResolutionErrors.dfy(372,10): Error: second argument to ==> must be of type bool
 ResolutionErrors.dfy(377,10): Error: first argument to ==> must be of type bool (instead got int)

 ResolutionErrors.dfy(377,10): Error: second argument to ==> must be of type bool (instead got int)

 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)

-62 resolution/type errors detected in ResolutionErrors.dfy

+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

+64 resolution/type errors detected in ResolutionErrors.dfy

 

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

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

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 7c919b2a..d5fecdf8 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -423,3 +423,27 @@ class Lamb {
   method Jesus() { }

   method Gwen() { }

 }

+

+// ------------------- assign-such-that and ghosts ------------------------------

+

+method AssignSuchThatFromGhost()

+{

+  var x: int;

+  ghost var g: int;

+

+  x := g;  // error: ghost cannot flow into non-ghost

+  

+  x := *;

+  assume x == g;  // this mix of ghosts and non-ghosts is cool (but, of course,

+                  // the compiler will complain)

+

+  x :| x == g;  // error: left-side has non-ghost, so RHS must be non-ghost as well

+

+  x :| assume x == g;  // this is cool, since it's an assume (but, of course, the

+                       // compiler will complain)

+

+  x :| x == 5;

+  g :| g <= g;

+  g :| assume g < g;  // the compiler will complain here, despite the LHS being

+                      // ghost -- and rightly so, since an assume is used

+}

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 7b409a67..43ee1d8e 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -530,7 +530,7 @@ method AssignSuchThat0(a: int, b: int) returns (x: int, y: int)
 

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

 {

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

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

   assert k == 0;

@@ -571,7 +571,7 @@ method AssignSuchThat4()
 

 method AssignSuchThat5()

 {

-  var n := new Node;

+  ghost var n := new Node;

   n :| fresh(n);  // fine

   assert false;  // error

 }

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 2dea7a52..42457918 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -101,10 +101,8 @@ method M()
   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;

+  k, m :| 0 <= k < m;  // error: LHS has non-ghost and RHS has ghost

   m :| m < 10;

 

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

diff --git a/Test/dafny2/StoreAndRetrieve.dfy b/Test/dafny2/StoreAndRetrieve.dfy
index da62f91c..d8938aa7 100644
--- a/Test/dafny2/StoreAndRetrieve.dfy
+++ b/Test/dafny2/StoreAndRetrieve.dfy
@@ -19,7 +19,7 @@ ghost module A {
       ensures Contents == old(Contents);

       ensures thing in Contents && L.Function.Apply(matchCriterion, thing);

     {

-      var k :| k in Contents && L.Function.Apply(matchCriterion, k);

+      var k :| assume k in Contents && L.Function.Apply(matchCriterion, k);

       thing := k;

     }

   }

@@ -52,7 +52,7 @@ module B refines A {
       }

       var k := arr[i];

       ...;

-      var a :| Contents == set x | x in a;

+      var a :| assume Contents == set x | x in a;

       arr := a;

     }

   }