diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-05-01 14:49:41 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-05-01 14:49:41 -0700 |
| commit | 9266a3c8da8825816bfd2b31aca9cec8aae0c455 (patch) | |
| tree | e87903cb141450e57b976c4dfca7057c2dbefb9a /Test/dafny0/Corecursion.dfy | |
| parent | bdf8ac6927bac67364dbc16422aa4d197c7f6e25 (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))
+ }
+}
+
+// --------------------------------------------------
|