diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-05-18 18:51:38 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-05-18 18:51:38 -0700 |
| commit | b185839df32bd15ddde7785b14dffc64f89a549b (patch) | |
| tree | 2fdd9fc42d664a37d8a6757278e7cd3a4e0a38db /Test/dafny0/Corecursion.dfy | |
| parent | 49f1ebd0391c4ecb346c7a98f14bf740fbe1f9a9 (diff) | |
Dafny: more correct checking of co-inductive productivity
Diffstat (limited to 'Test/dafny0/Corecursion.dfy')
| -rw-r--r-- | Test/dafny0/Corecursion.dfy | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/Test/dafny0/Corecursion.dfy b/Test/dafny0/Corecursion.dfy index decb68fc..9f1b1328 100644 --- a/Test/dafny0/Corecursion.dfy +++ b/Test/dafny0/Corecursion.dfy @@ -25,3 +25,28 @@ module CoRecursion { }
// --------------------------------------------------
+
+module CoRecursionNotUsed {
+ codatatype Stream<T> = More(T, Stream);
+
+ function F(s: Stream, n: nat): Stream
+ decreases n, true;
+ {
+ G(s, n)
+ }
+ function G(s: Stream, n: nat): Stream
+ decreases n, false;
+ {
+ if n == 0 then s else Tail(F(s, n-1))
+ }
+
+ function Tail(s: Stream): Stream
+ {
+ match s case More(hd, tl) => tl
+ }
+
+ function Diverge(n: nat): nat
+ {
+ Diverge(n) // error: cannot prove termination
+ }
+}
|