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
|
(** Some examples of mutual recursion and corresponding proofs of
termination *)
use int.Int
(** This example is from the book "Program Proofs" by Rustan Leino *)
let rec f1 (n: int) : int
requires { 0 <= n }
variant { n, 1 }
= if n = 0 then 0 else f2 n + 1
with f2 (n: int) : int
requires { 1 <= n }
variant { n, 0 }
= 2 * f1 (n - 1)
(** Hofstadter's Female and Male sequences *)
let rec function f (n: int) : int
requires { 0 <= n }
variant { n, 1 }
ensures { if n = 0 then result = 1 else 1 <= result <= n }
= if n = 0 then 1 else n - m (f (n - 1))
with function m (n: int) : int
requires { 0 <= n }
variant { n, 0 }
ensures { if n = 0 then result = 0 else 0 <= result < n }
= if n = 0 then 0 else n - f (m (n - 1))
|
