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

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";

+  }

 }