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

4 files changed, 10 insertions, 10 deletions

diff --git a/Chalice/examples/RockBand.chalice b/Chalice/examples/RockBand.chalice
index c7a2bba0..49b99a68 100644
--- a/Chalice/examples/RockBand.chalice
+++ b/Chalice/examples/RockBand.chalice
@@ -19,7 +19,7 @@ class RockBand module M {
     acc(gigs) && 0 <= gigs &&

     acc(gt) && gt != null && gt.Valid &&

     acc(gt.mu) &&  // to enable an eventual free

-    acc(doowops) && //forall{d: Vocalist in doowops; d != null && d.Valid} &&

+    acc(doowops) && //forall d: Vocalist in doowops :: d != null && d.Valid} &&

     acc(b3) && b3 != null && b3.Valid &&

     acc(b3.mu)  // to enable an eventual free

   }

diff --git a/Chalice/examples/iterator.chalice b/Chalice/examples/iterator.chalice
index 356e6d83..833a5a61 100644
--- a/Chalice/examples/iterator.chalice
+++ b/Chalice/examples/iterator.chalice
@@ -12,7 +12,7 @@ class List module Collections {
   method add(x: int) 

     requires valid;

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

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

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

   {

     unfold valid;

     contents := contents ++ [x];

@@ -21,7 +21,7 @@ class List module Collections {
 

   function get(index: int, f: int): int 

     requires 0<f && f<=100 && acc(valid, f) && (0<=index && index<size(f));

-    ensures forall { i in [1:f]; get(index, f) == get(index, i)};

+    ensures forall i in [1:f] :: get(index, f) == get(index, i);

   {

     unfolding acc(valid, f) in contents[index]

   }

@@ -29,7 +29,7 @@ class List module Collections {
   function size(f: int): int 

     requires 0<f && f<=100 && acc(valid, f);

     ensures 0<=result;

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

+    ensures forall i in [1:f] :: size(f) == size(i);

   {

     unfolding acc(valid, f) in |contents|

   }

@@ -147,4 +147,4 @@ class Program module Main {
     assert list.valid;

     assert list.size(50)==2;

   }

-}
\ No newline at end of file
+}

diff --git a/Chalice/examples/iterator2.chalice b/Chalice/examples/iterator2.chalice
index 5b75c1ca..f5a86909 100644
--- a/Chalice/examples/iterator2.chalice
+++ b/Chalice/examples/iterator2.chalice
@@ -14,7 +14,7 @@ class List module Collections {
   method add(x: int) 

     requires valid;

     ensures valid && size() == old(size()+1) && get(size()-1) == x; // I don't know why this happens.

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

@@ -131,4 +131,4 @@ class Program module Main {
     assert list.valid;

     assert list.size()==2;

   }

-}
\ No newline at end of file
+}

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