Chalice: added "exists" quantifier; changed surface syntax for quantifier expressions

1 files changed, 3 insertions, 3 deletions

diff --git a/Chalice/examples/producer-consumer.chalice b/Chalice/examples/producer-consumer.chalice
index 99756d65..11687e80 100644
--- a/Chalice/examples/producer-consumer.chalice
+++ b/Chalice/examples/producer-consumer.chalice
@@ -164,7 +164,7 @@ class List module Collections {
   method add(x: int) 

     requires valid;

     ensures valid && size() == old(size()+1) && get(size()-1) == x;

-    ensures forall { i in [0:size()-1]; get(i) == old(get(i)) };

+    ensures forall i in [0:size()-1] :: get(i) == old(get(i));

   {

     unfold valid;

     contents := contents ++ [x];

@@ -174,7 +174,7 @@ class List module Collections {
   method removeFirst() returns (rt: int) 

     requires valid && 0<size();

     ensures valid && size() == old(size()-1);

-    ensures forall { i  in [0:size()]; get(i) == old(get(i+1)) };

+    ensures forall i in [0:size()] :: get(i) == old(get(i+1));

   {

     unfold valid;

     rt := contents[0];

@@ -199,4 +199,4 @@ class List module Collections {
   predicate valid {

     acc(contents)

   }

-}
\ No newline at end of file
+}