diff options
| author |  Rustan Leino <unknown> | 2013-01-23 18:13:36 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-01-23 18:13:36 -0800 |
| commit | 1005adb004baf133b265eda5bfdc53022437e6ef (patch) | |
| tree | b2fd13051b5f484a79a9b2303404aafc2da5858f /Test/dafny0/Termination.dfy | |
| parent | 967bd4d7a4223d710f8f10659cdced173b249eac (diff) | |
Fixed bug in translation of method termination checks, and also fixed a (previously undetected) specification bug in the test suite.
Diffstat (limited to 'Test/dafny0/Termination.dfy')
| -rw-r--r-- | Test/dafny0/Termination.dfy | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy index 83baade1..45520b4a 100644 --- a/Test/dafny0/Termination.dfy +++ b/Test/dafny0/Termination.dfy @@ -410,3 +410,19 @@ module MapTests { {
}
}
+
+// --------------------- The following regression test case relies on the previous rank
+// --------------------- really being evaluated in the initial state
+
+class C {
+ var v: nat;
+ method Terminate()
+ modifies this;
+ decreases v;
+ {
+ if (v != 0) {
+ v := v - 1;
+ Terminate();
+ }
+ }
+}
|