diff options
| author |  mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
| commit | db6ef6c9e2bca859280cfbe17871c38da74977fc (patch) | |
| tree | d742312e6c9c69386f4c7111d9133ccc3d810e01 /Test/dafny0/Termination.dfy | |
Initial set of files.
Diffstat (limited to 'Test/dafny0/Termination.dfy')
| -rw-r--r-- | Test/dafny0/Termination.dfy | 80 |
1 files changed, 80 insertions, 0 deletions
diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy new file mode 100644 index 00000000..43fe63df --- /dev/null +++ b/Test/dafny0/Termination.dfy @@ -0,0 +1,80 @@ +class Termination {
+ method A(N: int)
+ requires 0 <= N;
+ {
+ var i := 0;
+ while (i < N)
+ invariant i <= N;
+ decreases N - i;
+ {
+ i := i + 1;
+ }
+ }
+
+ method B(N: int)
+ requires 0 <= N;
+ {
+ var i := N;
+ while (true)
+ invariant 0 <= i;
+ decreases i;
+ {
+ i := i - 1;
+ if (!(0 <= i)) {
+ break;
+ }
+ }
+ assert i == -1;
+ }
+
+ method Lex() {
+ var x: int, y: int;
+ call x := Update();
+ call y := Update();
+ while (!(x == 0 && y == 0))
+ invariant 0 <= x && 0 <= y;
+ decreases x, y;
+ {
+ if (0 < y) {
+ y := y - 1;
+ } else {
+ x := x - 1;
+ call y := Update();
+ }
+ }
+ }
+
+ method Update() returns (r: int)
+ ensures 0 <= r;
+ {
+ r := 8;
+ }
+
+ method M() {
+ var b := true;
+ var i := 500;
+ var r := new Termination;
+ var s := {12, 200};
+ var q := [5, 8, 13];
+ while (true)
+ decreases b, i, r;
+// invariant b ==> 0 <= i;
+ decreases s, q;
+ {
+ if (12 in s) {
+ s := s - {12};
+ } else if (b) {
+ b := !b;
+ i := i + 1;
+ } else if (20 <= i) {
+ i := i - 20;
+ } else if (r != null) {
+ r := null;
+ } else if (|q| != 0) {
+ q := q[1..];
+ } else {
+ break;
+ }
+ }
+ }
+}
|