summaryrefslogtreecommitdiff
path: root/Test/VSI-Benchmarks/b2.dfy
diff options
context:
space:
mode:
authorGravatar Rustan Leino <leino@microsoft.com>2011-05-26 00:02:57 -0700
committerGravatar Rustan Leino <leino@microsoft.com>2011-05-26 00:02:57 -0700
commitd9f2a82a417703f3669ba8399dcc8bcf34c3d742 (patch)
tree08b309fd809639a62c453c33dac86845dd4b9815 /Test/VSI-Benchmarks/b2.dfy
parente52270deab6d2fd5b885848211c2d9d1ab814b09 (diff)
Dafny: retired the "call" keyword
Diffstat (limited to 'Test/VSI-Benchmarks/b2.dfy')
-rw-r--r--Test/VSI-Benchmarks/b2.dfy16
1 files changed, 8 insertions, 8 deletions
diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy
index 6c6f11b3..3046621b 100644
--- a/Test/VSI-Benchmarks/b2.dfy
+++ b/Test/VSI-Benchmarks/b2.dfy
@@ -38,13 +38,13 @@ method Main() {
a[2] := -2;
a[3] := 0;
a[4] := 25;
- call TestSearch(a, 4);
- call TestSearch(a, -8);
- call TestSearch(a, -2);
- call TestSearch(a, 0);
- call TestSearch(a, 23);
- call TestSearch(a, 25);
- call TestSearch(a, 27);
+ TestSearch(a, 4);
+ TestSearch(a, -8);
+ TestSearch(a, -2);
+ TestSearch(a, 0);
+ TestSearch(a, 23);
+ TestSearch(a, 25);
+ TestSearch(a, 27);
}
method TestSearch(a: array<int>, key: int)
@@ -52,6 +52,6 @@ method TestSearch(a: array<int>, key: int)
requires (forall i, j :: 0 <= i && i < j && j < a.Length ==> a[i] <= a[j]);
{
var b := new Benchmark2;
- call r := b.BinarySearch(a, key);
+ var r := b.BinarySearch(a, key);
print "Looking for key=", key, ", result=", r, "\n";
}