diff options
author | 2012-05-01 14:49:41 -0700 | |
---|---|---|
committer | 2012-05-01 14:49:41 -0700 | |
commit | e956452c717924a6a945fd57229cfce1d16e686f (patch) | |
tree | a3cee63b3103a52e771b3c0a573d6e970692fa63 /Test/dafny0/Corecursion.dfy | |
parent | 8060f754c82b0b23fac567978c756d7897cb0471 (diff) |
Dafny: added support for co-recursive calls
Diffstat (limited to 'Test/dafny0/Corecursion.dfy')
-rw-r--r-- | Test/dafny0/Corecursion.dfy | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/Test/dafny0/Corecursion.dfy b/Test/dafny0/Corecursion.dfy new file mode 100644 index 00000000..decb68fc --- /dev/null +++ b/Test/dafny0/Corecursion.dfy @@ -0,0 +1,27 @@ +
+// --------------------------------------------------
+
+module CoRecursion {
+ codatatype Stream<T> = More(head: T, rest: Stream);
+
+ function AscendingChain(n: int): Stream<int>
+ {
+ More(n, AscendingChain(n+1))
+ }
+
+ function AscendingChainAndRead(n: int): Stream<int>
+ reads this; // with a reads clause, this function is not a co-recusvie function
+ {
+ More(n, AscendingChainAndRead(n+1)) // error: cannot prove termination
+ }
+
+ datatype List<T> = Nil | Cons(T, List);
+
+ function Prefix(n: nat, s: Stream): List
+ {
+ if n == 0 then Nil else
+ Cons(s.head, Prefix(n-1, s.rest))
+ }
+}
+
+// --------------------------------------------------
|