diff options
Diffstat (limited to 'Test/dafny3/SimpleInduction.dfy')
-rw-r--r-- | Test/dafny3/SimpleInduction.dfy | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Test/dafny3/SimpleInduction.dfy b/Test/dafny3/SimpleInduction.dfy index 5331b808..700b531c 100644 --- a/Test/dafny3/SimpleInduction.dfy +++ b/Test/dafny3/SimpleInduction.dfy @@ -22,7 +22,7 @@ ghost method FibLemma(n: nat) }
/*
- The 'parallel' statement has the effect of applying its body simultaneously
+ The 'forall' statement has the effect of applying its body simultaneously
to all values of the bound variables---in the first example, to all k
satisfying 0 <= k < n, and in the second example, to all non-negative n.
*/
@@ -30,7 +30,7 @@ ghost method FibLemma(n: nat) ghost method FibLemma_Alternative(n: nat)
ensures Fib(n) % 2 == 0 <==> n % 3 == 0;
{
- parallel (k | 0 <= k < n) {
+ forall k | 0 <= k < n {
FibLemma_Alternative(k);
}
}
@@ -38,7 +38,7 @@ ghost method FibLemma_Alternative(n: nat) ghost method FibLemma_All()
ensures forall n :: 0 <= n ==> (Fib(n) % 2 == 0 <==> n % 3 == 0);
{
- parallel (n | 0 <= n) {
+ forall n | 0 <= n {
FibLemma(n);
}
}
|