diff options
| author |  Rustan Leino <leino@microsoft.com> | 2013-01-20 14:02:09 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2013-01-20 14:02:09 -0800 |
| commit | 724cd08bb69546967483e13fdd1a7c7b9797f59b (patch) | |
| tree | e0f7cf732ba1daf05b7e574bf57e723d0c5ef7b8 /Test/dafny0/CoPrefix.dfy | |
| parent | 0f380d0d99aa2439b59814ec43305bc18cb0ff64 (diff) | |
Added some co- test cases. Fixed some bugs.
Diffstat (limited to 'Test/dafny0/CoPrefix.dfy')
| -rw-r--r-- | Test/dafny0/CoPrefix.dfy | 41 |
1 files changed, 41 insertions, 0 deletions
diff --git a/Test/dafny0/CoPrefix.dfy b/Test/dafny0/CoPrefix.dfy index 991e160f..d3cecc28 100644 --- a/Test/dafny0/CoPrefix.dfy +++ b/Test/dafny0/CoPrefix.dfy @@ -148,3 +148,44 @@ comethod {:induction false} BadTheorem(s: IList) { // error: postcondition violation
BadTheorem(s.tail);
}
+
+// ---------------------------------
+
+// Make sure recursive calls get checked for termination
+module Recursion {
+ comethod X() { Y(); }
+ comethod Y() { X(); }
+
+ comethod G(x: int)
+ ensures x < 100;
+ { // error: postcondition violation (when _k == 0)
+ H(x);
+ }
+ comethod H(x: int)
+ ensures x < 100;
+ { // error: postcondition violation (when _k == 0)
+ G(x);
+ }
+
+ comethod A(x: int) { B(x); }
+ comethod B(x: int)
+ {
+ A#[10](x); // error: this is a recursive call, and the termination metric may not be going down
+ }
+
+ comethod A'(x: int) { B'(x); }
+ comethod B'(x: int)
+ {
+ if (10 < _k) {
+ A'#[10](x);
+ }
+ }
+
+ comethod A''(x: int) { B''(x); }
+ comethod B''(x: int)
+ {
+ if (0 < x) {
+ A''#[_k](x-1);
+ }
+ }
+}
|