diff options
author | rustanleino <unknown> | 2010-05-06 20:28:29 +0000 |
---|---|---|
committer | rustanleino <unknown> | 2010-05-06 20:28:29 +0000 |
commit | 9973fcca56f1c6345ac2697210f2f3c7662f5c30 (patch) | |
tree | abab0acad6a0ee4d8f93cda6d84a75fa73af5dbe /Test/VSI-Benchmarks/b1.dfy | |
parent | b50b9e5c715cc9c94496418d5adc4023bef6516c (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";
+ }
}
|