diff options
| author |  rustanleino <unknown> | 2010-06-11 02:02:36 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-06-11 02:02:36 +0000 |
| commit | fadc6a922eb99b83b898b55286e48f63ed0df751 (patch) | |
| tree | 8aa3e8fa417e79fdfc96502ddcb5a5fdc13c7927 /Test/VSI-Benchmarks/b1.dfy | |
| parent | 9521767199e98aafb780421b859da3fb8773af42 (diff) | |
Dafny: Added two additional heuristics for guessing missing loop decreases clauses (for loop guard A!=B and for loop guards with multiple conjuncts)
Diffstat (limited to 'Test/VSI-Benchmarks/b1.dfy')
| -rw-r--r-- | Test/VSI-Benchmarks/b1.dfy | 122 |
1 files changed, 59 insertions, 63 deletions
diff --git a/Test/VSI-Benchmarks/b1.dfy b/Test/VSI-Benchmarks/b1.dfy index 1ab76a78..cd4a18c2 100644 --- a/Test/VSI-Benchmarks/b1.dfy +++ b/Test/VSI-Benchmarks/b1.dfy @@ -1,75 +1,71 @@ -// 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.
+// for any kind of termination. Also, in Spec#, there
+// is an issue of potential overflows.
+
+// Benchmark1
-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 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;
+ {
+ r := r - 1;
+ n := n + 1;
+ }
+ } else {
+ var n := y;
+ while (n != 0)
+ invariant r == x+y-n && 0 <= n;
+ {
+ r := r + 1;
+ n := n - 1;
}
}
+}
- method Mul(x: int, y: int) returns (r: int)
- ensures r == x*y;
- decreases x < 0, x;
- {
- if (x == 0) {
- r := 0;
- } else if (x < 0) {
- call r := Mul(-x, y);
- r := -r;
- } else {
- call r := Mul(x-1, y);
- call r := Add(r, y);
- }
+method Mul(x: int, y: int) returns (r: int)
+ ensures r == x*y;
+ decreases x < 0, x;
+{
+ if (x == 0) {
+ r := 0;
+ } else if (x < 0) {
+ call r := Mul(-x, y);
+ r := -r;
+ } else {
+ call r := Mul(x-1, y);
+ 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 Main() {
+ call TestAdd(3, 180);
+ call TestAdd(3, -180);
+ call TestAdd(0, 1);
- method TestAdd(x: int, y: int) {
- print x, " + ", y, " = ";
- call z := Add(x, y);
- print z, "\n";
- }
+ 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 TestMul(x: int, y: int) {
- print x, " * ", y, " = ";
- call z := Mul(x, y);
- print z, "\n";
- }
+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";
}
|