The "choose" statement, hacky and specialized as it was, is now gone. Use the assign-such-that statement instead. For example: x :| x in S;

7 files changed, 27 insertions, 34 deletions

diff --git a/Test/dafny0/AdvancedLHS.dfy b/Test/dafny0/AdvancedLHS.dfy
index f1fc7d48..51e9b769 100644
--- a/Test/dafny0/AdvancedLHS.dfy
+++ b/Test/dafny0/AdvancedLHS.dfy
@@ -8,7 +8,6 @@ class C {
     x := new C;

     x := new C.Init();

     x := *;

-    x := choose S;

 

     // test evaluation order

     var c := x;

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index a2b3afba..0ca8c4f8 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -589,7 +589,7 @@ NonGhostQuantifiers.dfy(137,8): Error: Assignment to non-ghost variable is not a
 20 resolution/type errors detected in NonGhostQuantifiers.dfy

 

 -------------------- AdvancedLHS.dfy --------------------

-AdvancedLHS.dfy(32,23): Error: target object may be null

+AdvancedLHS.dfy(31,23): Error: target object may be null

 Execution trace:

     (0,0): anon0

     (0,0): anon15_Else

@@ -981,25 +981,24 @@ ParallelResolveErrors.dfy(7,9): Error: Assignment to non-ghost field is not allo
 ParallelResolveErrors.dfy(18,6): Error: LHS of assignment must denote a mutable variable or field

 ParallelResolveErrors.dfy(23,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement

 ParallelResolveErrors.dfy(41,6): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

-ParallelResolveErrors.dfy(53,13): Error: set choose operator not supported inside the enclosing forall statement

-ParallelResolveErrors.dfy(58,13): Error: new allocation not supported in forall statements

-ParallelResolveErrors.dfy(63,13): Error: new allocation not allowed in ghost context

-ParallelResolveErrors.dfy(64,13): Error: new allocation not allowed in ghost context

-ParallelResolveErrors.dfy(65,13): Error: new allocation not allowed in ghost context

-ParallelResolveErrors.dfy(66,13): Error: new allocation not allowed in ghost context

-ParallelResolveErrors.dfy(67,6): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause

-ParallelResolveErrors.dfy(68,6): Error: the body of the enclosing forall statement is not allowed to call non-ghost methods

-ParallelResolveErrors.dfy(75,19): Error: trying to break out of more loop levels than there are enclosing loops

-ParallelResolveErrors.dfy(79,18): Error: return statement is not allowed inside a forall statement

-ParallelResolveErrors.dfy(86,21): Error: trying to break out of more loop levels than there are enclosing loops

-ParallelResolveErrors.dfy(87,20): Error: trying to break out of more loop levels than there are enclosing loops

-ParallelResolveErrors.dfy(88,20): Error: break label is undefined or not in scope: OutsideLoop

-ParallelResolveErrors.dfy(97,24): Error: trying to break out of more loop levels than there are enclosing loops

-ParallelResolveErrors.dfy(98,24): Error: break label is undefined or not in scope: OutsideLoop

-ParallelResolveErrors.dfy(109,9): Error: the body of the enclosing forall statement is not allowed to update heap locations

+ParallelResolveErrors.dfy(53,13): Error: new allocation not supported in forall statements

+ParallelResolveErrors.dfy(58,13): Error: new allocation not allowed in ghost context

+ParallelResolveErrors.dfy(59,13): Error: new allocation not allowed in ghost context

+ParallelResolveErrors.dfy(60,13): Error: new allocation not allowed in ghost context

+ParallelResolveErrors.dfy(61,13): Error: new allocation not allowed in ghost context

+ParallelResolveErrors.dfy(62,6): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause

+ParallelResolveErrors.dfy(63,6): Error: the body of the enclosing forall statement is not allowed to call non-ghost methods

+ParallelResolveErrors.dfy(70,19): Error: trying to break out of more loop levels than there are enclosing loops

+ParallelResolveErrors.dfy(74,18): Error: return statement is not allowed inside a forall statement

+ParallelResolveErrors.dfy(81,21): Error: trying to break out of more loop levels than there are enclosing loops

+ParallelResolveErrors.dfy(82,20): Error: trying to break out of more loop levels than there are enclosing loops

+ParallelResolveErrors.dfy(83,20): Error: break label is undefined or not in scope: OutsideLoop

+ParallelResolveErrors.dfy(92,24): Error: trying to break out of more loop levels than there are enclosing loops

+ParallelResolveErrors.dfy(93,24): Error: break label is undefined or not in scope: OutsideLoop

+ParallelResolveErrors.dfy(104,9): Error: the body of the enclosing forall statement is not allowed to update heap locations

+ParallelResolveErrors.dfy(112,6): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause

 ParallelResolveErrors.dfy(117,6): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause

-ParallelResolveErrors.dfy(122,6): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause

-22 resolution/type errors detected in ParallelResolveErrors.dfy

+21 resolution/type errors detected in ParallelResolveErrors.dfy

 

 -------------------- Parallel.dfy --------------------

 Parallel.dfy(31,5): Error BP5002: A precondition for this call might not hold.

diff --git a/Test/dafny0/Comprehensions.dfy b/Test/dafny0/Comprehensions.dfy
index ca1fcfb7..24015fc6 100644
--- a/Test/dafny0/Comprehensions.dfy
+++ b/Test/dafny0/Comprehensions.dfy
@@ -35,7 +35,7 @@ method PrintSet<T>(s: set<T>) {
   while (q != {})

     decreases q;

   {

-    var x := choose q;

+    var x :| x in q;

     print x, " ";

     q := q - {x};

   }

diff --git a/Test/dafny0/LoopModifies.dfy b/Test/dafny0/LoopModifies.dfy
index c9d87f86..1757836f 100644
--- a/Test/dafny0/LoopModifies.dfy
+++ b/Test/dafny0/LoopModifies.dfy
@@ -307,7 +307,7 @@ method Testing12(a: Elem, b: Elem, c: Elem)
       modifies S;

       decreases S;

    {

-      var j := choose S;

+      var j :| j in S;

       // these still good, even though S shrinks to not include them.

       a.i := i;

       b.i := i;

diff --git a/Test/dafny0/ParallelResolveErrors.dfy b/Test/dafny0/ParallelResolveErrors.dfy
index d3bfe97b..affc765d 100644
--- a/Test/dafny0/ParallelResolveErrors.dfy
+++ b/Test/dafny0/ParallelResolveErrors.dfy
@@ -48,11 +48,6 @@ method M0(IS: set<int>)
     x := x + 1;  // cool

   }

 

-  var ia := new int[20];

-  forall (i | 0 <= i < 20) {

-    ia[i] := choose IS;  // error: set choose not allowed

-  }

-

   var ca := new C[20];

   forall (i | 0 <= i < 20) {

     ca[i] := new C;  // error: new allocation not allowed

diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy
index 4c761671..a4043f4d 100644
--- a/Test/dafny1/Celebrity.dfy
+++ b/Test/dafny1/Celebrity.dfy
@@ -22,20 +22,20 @@ method FindCelebrity1<Person>(people: set<Person>, ghost c: Person) returns (r:
   ensures r == c;

 {

   var Q := people;

-  var x := choose Q;

+  var x :| x in Q;

   while (Q != {x})

     //invariant Q <= people;  // inv1 in Rodin's Celebrity_1, but it's not needed here

     invariant IsCelebrity(c, Q);  // inv2

     invariant x in Q;

     decreases Q;

   {

-    var y := choose Q - {x};

+    var y :| y in Q - {x};

     if (Knows(x, y)) {

       Q := Q - {x};  // remove_1

     } else {

       Q := Q - {y};  assert x in Q;  // remove_2

     }

-    x := choose Q;

+    x :| x in Q;

   }

   r := x;

 }

@@ -44,7 +44,7 @@ method FindCelebrity2<Person>(people: set<Person>, ghost c: Person) returns (r:
   requires IsCelebrity(c, people);

   ensures r == c;

 {

-  var b := choose people;

+  var b :| b in people;

   var R := people - {b};

   while (R != {})

     invariant R <= people;  // inv1

@@ -54,7 +54,7 @@ method FindCelebrity2<Person>(people: set<Person>, ghost c: Person) returns (r:
 

     decreases R;

   {

-    var x := choose R;

+    var x :| x in R;

     if (Knows(x, b)) {

       R := R - {x};

     } else {

diff --git a/Test/vstte2012/BreadthFirstSearch.dfy b/Test/vstte2012/BreadthFirstSearch.dfy
index e1a93730..ac070ac6 100644
--- a/Test/vstte2012/BreadthFirstSearch.dfy
+++ b/Test/vstte2012/BreadthFirstSearch.dfy
@@ -80,7 +80,7 @@ class BreadthFirstSearch<Vertex(==)>
       decreases AllVertices - Processed;

     {

       // remove a vertex "v" from "C"

-      var v := choose C;

+      var v :| v in C;

       C, Processed := C - {v}, Processed + {v};

       ghost var pathToV := Find(source, v, paths);

     

@@ -264,7 +264,7 @@ class BreadthFirstSearch<Vertex(==)>
     if (vSuccs == {}) {

       newPaths := paths;

     } else {

-      var succ := choose vSuccs;

+      var succ :| succ in vSuccs;

       newPaths := Maplet(Domain(paths) + {succ}, succ, pathToV + [v], paths);

       newPaths := UpdatePaths(vSuccs - {succ}, source, newPaths, v, pathToV);

     }