diff options
author | 2011-05-26 00:02:57 -0700 | |
---|---|---|
committer | 2011-05-26 00:02:57 -0700 | |
commit | a7731599b7ab802c7c47e5ccf33e21953a238c2d (patch) | |
tree | af68f595ddddfc2195487f90754080635038fe24 /Test/VSI-Benchmarks/b2.dfy | |
parent | daba6b774c3f945de58229f28078e8dccaaec782 (diff) |
Dafny: retired the "call" keyword
Diffstat (limited to 'Test/VSI-Benchmarks/b2.dfy')
-rw-r--r-- | Test/VSI-Benchmarks/b2.dfy | 16 |
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";
}
|