diff options
Diffstat (limited to 'Chalice/examples')
-rw-r--r-- | Chalice/examples/RockBand.chalice | 2 | ||||
-rw-r--r-- | Chalice/examples/iterator.chalice | 8 | ||||
-rw-r--r-- | Chalice/examples/iterator2.chalice | 4 | ||||
-rw-r--r-- | Chalice/examples/producer-consumer.chalice | 6 |
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 +}
|