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 | c606bc377095f9ef0a7587cab58e90cca82b29f0 (patch) | |
| tree | 3911d5ea379d82cee069e9715e3ea710ef49107e /Test/dafny0/Corecursion.dfy | |
| parent | 4eac6913448c492602c9ccef20d0ee6d0a7194cc (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
+ }
+}
|