summaryrefslogtreecommitdiff
path: root/Test/dafny0/Corecursion.dfy
blob: 0918d6f5e2903cb1034ffa83a5e604773e2fe968 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52

// --------------------------------------------------

module CoRecursion {
  codatatype Stream<T> = More(head: T, rest: Stream);

  function AscendingChain(n: int): Stream<int>
  {
    More(n, AscendingChain(n+1))
  }

  function AscendingChainAndRead(n: nat): 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))
  }
}

// --------------------------------------------------

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
  }
}