## Mutual recursion

Some examples of mutual recursion and corresponding proofs of termination

**Authors:** Jean-Christophe Filliâtre

**Topics:** Tricky termination

**Tools:** Why3

see also the index (by topic, by tool, by reference, by year)

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

download ZIP archive

# Why3 Proof Results for Project "mutual_recursion"

## Theory "mutual_recursion.Top": fully verified

Obligations | Alt-Ergo 2.3.0 | |||

VC for f1 | 0.00 | |||

VC for f2 | 0.01 | |||

VC for f | --- | |||

split_vc | ||||

variant decrease | 0.00 | |||

precondition | 0.00 | |||

variant decrease | 0.00 | |||

precondition | 0.00 | |||

postcondition | --- | |||

split_vc | ||||

postcondition | 0.00 | |||

postcondition | --- | |||

split_vc | ||||

postcondition | 0.00 | |||

postcondition | 0.00 | |||

postcondition | 0.00 | |||

VC for m | --- | |||

split_vc | ||||

variant decrease | 0.00 | |||

precondition | 0.00 | |||

variant decrease | 0.00 | |||

precondition | 0.00 | |||

postcondition | --- | |||

split_vc | ||||

postcondition | --- | |||

split_vc | ||||

postcondition | 0.00 | |||

postcondition | 0.00 | |||

postcondition | 0.00 | |||

postcondition | 0.00 |