diff options
author | 2010-05-06 20:28:29 +0000 | |
---|---|---|
committer | 2010-05-06 20:28:29 +0000 | |
commit | a2f70f46e1a4dfb513df45657178399269cec67d (patch) | |
tree | bacc4d411170492170faa80fd619a009da602650 /Test/VSI-Benchmarks/b1.dfy | |
parent | e9c25e761ad3a5e31e077f7bb595bfc10618c2bb (diff) |
Dafny:
* First crack at a compiler (/compile:1 writes out.cs, if Dafny program verifies)
* Added "print" statement (to make running compiled programs more interesting)
* Changed name of default class from $default to _default
Boogie:
* Included "lambda" as a keyword in emacs and latex style files
Diffstat (limited to 'Test/VSI-Benchmarks/b1.dfy')
-rw-r--r-- | Test/VSI-Benchmarks/b1.dfy | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/Test/VSI-Benchmarks/b1.dfy b/Test/VSI-Benchmarks/b1.dfy index 70522aaf..1ab76a78 100644 --- a/Test/VSI-Benchmarks/b1.dfy +++ b/Test/VSI-Benchmarks/b1.dfy @@ -47,4 +47,29 @@ class Benchmark1 { call r := Add(r, y);
}
}
+
+ method Main() {
+ call TestAdd(3, 180);
+ call TestAdd(3, -180);
+ call 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);
+ }
+
+ method TestAdd(x: int, y: int) {
+ print x, " + ", y, " = ";
+ call z := Add(x, y);
+ print z, "\n";
+ }
+
+ method TestMul(x: int, y: int) {
+ print x, " * ", y, " = ";
+ call z := Mul(x, y);
+ print z, "\n";
+ }
}
|