diff options
| author |  rustanleino <unknown> | 2010-06-24 00:41:04 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-06-24 00:41:04 +0000 |
| commit | cf26b0336a404760302bd57eb822fa906105cf1d (patch) | |
| tree | 7043f794c473404d8895af7946c302e258dd1fd6 /Test/dafny0 | |
| parent | 67c07706d2b4ee941954301a0c18abfcf253384c (diff) | |
Dafny:
* For every loop decreases clause N, generate a free loop invariant N <= N0, where N0 is the value of N just before the loop.
* Added Test/dafny1/KatzManna.dfy, which contains the 3 programs (and their termination annotations) from the Katz and Manna 1975 paper "A closer look at termination" (which benefits from the feature above).
Diffstat (limited to 'Test/dafny0')
| -rw-r--r-- | Test/dafny0/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny0/Termination.dfy | 22 |
2 files changed, 23 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 34b15b8a..0581fe6b 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -372,7 +372,7 @@ Execution trace: Termination.dfy(119,16): anon9_Else
(0,0): anon5
-Dafny program verifier finished with 23 verified, 4 errors
+Dafny program verifier finished with 25 verified, 4 errors
-------------------- Use.dfy --------------------
Use.dfy(16,18): Error: assertion violation
diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy index 974dadab..35ff53b0 100644 --- a/Test/dafny0/Termination.dfy +++ b/Test/dafny0/Termination.dfy @@ -170,3 +170,25 @@ class Node { next.Valid())
}
}
+
+method DecreasesYieldsAnInvariant(z: int) {
+ var x := 100;
+ var y := 1;
+ var z := z; // make parameter into a local variable
+ while (x != y)
+ // inferred: decreases |x - y|;
+ invariant (0 < x && 0 < y) || (x < 0 && y < 0);
+ {
+ if (z == 52) {
+ break;
+ } else if (x < y) {
+ y := y - 1;
+ } else {
+ x := x - 1;
+ }
+ x := -x;
+ y := -y;
+ z := z + 1;
+ }
+ assert x - y < 100; // follows from the fact that no loop iteration increases what's in the 'decreases' clause
+}
|