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/VSI-Benchmarks/b1.dfy | |
| parent | e52270deab6d2fd5b885848211c2d9d1ab814b09 (diff) | |
Dafny: retired the "call" keyword
Diffstat (limited to 'Test/VSI-Benchmarks/b1.dfy')
| -rw-r--r-- | Test/VSI-Benchmarks/b1.dfy | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/Test/VSI-Benchmarks/b1.dfy b/Test/VSI-Benchmarks/b1.dfy index cd4a18c2..3bd2bf43 100644 --- a/Test/VSI-Benchmarks/b1.dfy +++ b/Test/VSI-Benchmarks/b1.dfy @@ -35,37 +35,37 @@ method Mul(x: int, y: int) returns (r: int) if (x == 0) {
r := 0;
} else if (x < 0) {
- call r := Mul(-x, y);
+ r := Mul(-x, y);
r := -r;
} else {
- call r := Mul(x-1, y);
- call r := Add(r, y);
+ r := Mul(x-1, y);
+ r := Add(r, y);
}
}
// ---------------------------
method Main() {
- call TestAdd(3, 180);
- call TestAdd(3, -180);
- call TestAdd(0, 1);
+ TestAdd(3, 180);
+ TestAdd(3, -180);
+ TestAdd(0, 1);
- call TestMul(3, 180);
- call TestMul(3, -180);
- call TestMul(180, 3);
- call TestMul(-180, 3);
- call TestMul(0, 1);
- call TestMul(1, 0);
+ TestMul(3, 180);
+ TestMul(3, -180);
+ TestMul(180, 3);
+ TestMul(-180, 3);
+ TestMul(0, 1);
+ TestMul(1, 0);
}
method TestAdd(x: int, y: int) {
print x, " + ", y, " = ";
- call z := Add(x, y);
+ var z := Add(x, y);
print z, "\n";
}
method TestMul(x: int, y: int) {
print x, " * ", y, " = ";
- call z := Mul(x, y);
+ var z := Mul(x, y);
print z, "\n";
}
|