examples/mutual_recursion.mlw

   1
   2 (** Some examples of mutual recursion and corresponding proofs of
   3     termination *)
   4
   5 use int.Int
   6
   7 (** This example is from the book "Program Proofs" by Rustan Leino *)
   8
   9 let rec f1 (n: int) : int
  10   requires { 0 <= n }
  11   variant  { n, 1 }
  12 = if n = 0 then 0 else f2 n + 1
  13
  14 with f2 (n: int) : int
  15   requires { 1 <= n }
  16   variant  { n, 0 }
  17 = 2 * f1 (n - 1)
  18
  19 (** Hofstadter's Female and Male sequences *)
  20
  21 let rec function f (n: int) : int
  22   requires { 0 <= n }
  23   variant  { n, 1 }
  24   ensures  { if n = 0 then result = 1  else 1 <= result <= n }
  25 = if n = 0 then 1 else n - m (f (n - 1))
  26
  27 with function m (n: int) : int
  28   requires { 0 <= n }
  29   variant  { n, 0 }
  30   ensures  { if n = 0 then result = 0 else 0 <= result < n }
  31 = if n = 0 then 0 else n - f (m (n - 1))