diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-05-26 00:02:57 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-05-26 00:02:57 -0700 |
| commit | d9f2a82a417703f3669ba8399dcc8bcf34c3d742 (patch) | |
| tree | 08b309fd809639a62c453c33dac86845dd4b9815 /Test/dafny1/pow2.dfy | |
| parent | e52270deab6d2fd5b885848211c2d9d1ab814b09 (diff) | |
Dafny: retired the "call" keyword
Diffstat (limited to 'Test/dafny1/pow2.dfy')
| -rw-r--r-- | Test/dafny1/pow2.dfy | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/Test/dafny1/pow2.dfy b/Test/dafny1/pow2.dfy index 52cddaac..c7e4bc63 100644 --- a/Test/dafny1/pow2.dfy +++ b/Test/dafny1/pow2.dfy @@ -36,7 +36,7 @@ ghost method Lemma(n: int) ensures pow2_slow(n) == Square(pow2_slow(n/2));
{
if (n != 0) {
- call Lemma(n-2);
+ Lemma(n-2);
}
}
@@ -46,9 +46,9 @@ ghost method Theorem(n: int) {
if (n == 0) {
} else if (IsEven(n)) {
- call Lemma(n);
- call Theorem(n/2);
+ Lemma(n);
+ Theorem(n/2);
} else {
- call Theorem(n-1);
+ Theorem(n-1);
}
}
|