diff options
| author |  RMonahan <unknown> | 2009-10-30 23:52:13 +0000 |
|---|---|---|
| committer | RMonahan <unknown> | 2009-10-30 23:52:13 +0000 |
| commit | cb32052c7ae22c970d5db7dd51881845adfa66d2 (patch) | |
| tree | 2ebc190bc336ed412f6b39c1b131f01644f70faf /Test/VSI-Benchmarks/b1.dfy | |
| parent | 58795baa8bff26cdb4430b90e69395abf52c4161 (diff) | |
Initial version of VSI Benchmarks 1 - 8
Diffstat (limited to 'Test/VSI-Benchmarks/b1.dfy')
| -rw-r--r-- | Test/VSI-Benchmarks/b1.dfy | 47 |
1 files changed, 47 insertions, 0 deletions
diff --git a/Test/VSI-Benchmarks/b1.dfy b/Test/VSI-Benchmarks/b1.dfy new file mode 100644 index 00000000..ba293008 --- /dev/null +++ b/Test/VSI-Benchmarks/b1.dfy @@ -0,0 +1,47 @@ +// Note: To prove termination of calls, methods need
+// a termination measure, but Dafny does not yet support
+// termination measures for methods (but it will in
+// the foreseeable future).
+
+// Spec# and Boogie and Chalice: The program will be
+// the same, except that these languages do not check
+// for any kind of termination.
+
+class Benchmark1 {
+ method Add(x: int, y: int) returns (r: int)
+ ensures r == x+y;
+ {
+ r := x;
+ if (y < 0) {
+ var n := y;
+ while (n != 0)
+ invariant r == x+y-n && 0 <= -n;
+ decreases -n;
+ {
+ r := r - 1;
+ n := n + 1;
+ }
+ } else {
+ var n := y;
+ while (n != 0)
+ invariant r == x+y-n && 0 <= n;
+ decreases n;
+ {
+ r := r + 1;
+ n := n - 1;
+ }
+ }
+ }
+
+ method Mul(x: int, y: int) returns (r: int)
+ ensures r == x*y;
+ {
+ if (x < 0) {
+ call r := Mul(-x, y);
+ r := -r;
+ } else {
+ call r := Mul(x-1, y);
+ call r := Add(r, y);
+ }
+ }
+}
|