## Towers of Hanoi

Classical recursive algorithm

Topics: Ghost code

Tools: Why3

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

```module Hanoi
(* a simple version where the disks are natural numbers from 1 to n *)

use int.Int
use list.List
use list.Length
use list.SortedInt

type tower = {
mutable rod : list int;
} invariant {
sorted rod
}

function prepend (n: int) (s: list int) : list int

axiom prepend_def_zero :
forall s: list int, n: int.
n <= 0 -> prepend n s = s

axiom prepend_def_succ :
forall s: list int, n: int.
n > 0 -> prepend n s = prepend (n - 1) (Cons n s)

let move (a b: tower) (ghost n: int) (ghost s: list int)
requires { a.rod = Cons n s }
requires { match b.rod with Nil -> true | Cons x _ -> x > n end }
ensures  { a.rod = s }
ensures  { b.rod = Cons n (old b.rod) }
= match a.rod with
| Cons x r ->
a.rod <- r;
b.rod <- Cons x b.rod
| Nil -> absurd
end

let rec hanoi_rec (a b c: tower) (n: int) (ghost s: list int)
requires { a.rod = prepend n s }
requires { match b.rod with Nil -> true | Cons x _ -> x > n end }
requires { match c.rod with Nil -> true | Cons x _ -> x > n end }
variant  { n }
ensures  { a.rod = s }
ensures  { b.rod = prepend n (old b.rod) }
ensures  { c.rod = old c.rod }
= if n > 0 then begin
let ghost t = c.rod in
hanoi_rec a c b (n-1) (Cons n s);
move a b n s;
hanoi_rec c b a (n-1) t
end

let tower_of_hanoi (a b c: tower)
requires { a.rod = prepend (length a.rod) Nil }
requires { b.rod = c.rod = Nil }
ensures  { b.rod = old a.rod }
ensures  { a.rod = c.rod = Nil }
= hanoi_rec a b c (length a.rod) Nil

end

module Tower_of_Hanoi
(* a generalized version where the disks are arbitrary integers *)

use int.Int
use list.List
use list.Length

use list.RevAppend
clone list.RevSorted with type t = int, predicate le = (<),
goal Transitive.Trans

type tower = {
mutable rod : list int;
} invariant {
Incr.sorted rod
}

let move (a b: tower) (ghost x: int) (ghost s: list int)
requires { a.rod = Cons x s }
requires { match b.rod with Nil -> true | Cons y _ -> x < y end }
ensures  { a.rod = s }
ensures  { b.rod = Cons x (old b.rod) }
= match a.rod with
| Cons x r ->
a.rod <- r;
b.rod <- Cons x b.rod
| Nil -> absurd
end

let rec hanoi_rec (a b c: tower) (n: int) (ghost p s: list int)
requires { length p = n /\ Decr.sorted p }
requires { a.rod = rev_append p s }
requires { compat p b.rod }
requires { compat p c.rod }
variant  { n }
ensures  { a.rod = s }
ensures  { b.rod = rev_append p (old b.rod) }
ensures  { c.rod = old c.rod }
= if n > 0 then begin
let ghost t = c.rod in
let x,r = match p with Cons x r -> x,r | Nil -> absurd end in
hanoi_rec a c b (n-1) r (Cons x s);
move a b x s;
hanoi_rec c b a (n-1) r t
end

let tower_of_hanoi (a b c: tower)
requires { b.rod = c.rod = Nil }
ensures  { b.rod = old a.rod }
ensures  { a.rod = c.rod = Nil }
= hanoi_rec a b c (length a.rod) (ghost rev_append a.rod Nil) Nil

end
```

# Why3 Proof Results for Project "tower_of_hanoi"

## Theory "tower_of_hanoi.Hanoi": fully verified

 Obligations Alt-Ergo 2.1.0 VC for tower 0.00 VC for move --- split_goal_right type invariant 0.01 type invariant 0.02 postcondition 0.01 postcondition 0.01 unreachable point 0.00 VC for hanoi_rec --- split_goal_right variant decrease 0.00 precondition 0.01 precondition 0.01 precondition 0.02 precondition 0.00 precondition 0.01 variant decrease 0.00 precondition 0.00 precondition 0.00 precondition 0.33 postcondition 0.01 postcondition 0.01 postcondition 0.01 postcondition 0.00 postcondition 0.00 postcondition 0.00 VC for tower_of_hanoi --- split_goal_right precondition 0.00 precondition 0.00 precondition 0.01 postcondition 0.00 postcondition 0.00

## Theory "tower_of_hanoi.Tower_of_Hanoi": fully verified

 Obligations Alt-Ergo 2.1.0 Alt-Ergo 2.3.0 RevSorted.Transitive.Trans 0.00 --- VC for tower 0.00 --- VC for move --- --- split_goal_right type invariant 0.01 --- type invariant 0.03 --- postcondition 0.01 --- postcondition 0.02 --- unreachable point 0.01 --- VC for hanoi_rec --- --- split_goal_right unreachable point 0.01 --- variant decrease 0.01 --- precondition 0.02 --- precondition 0.01 --- precondition 0.95 --- precondition --- 1.12 precondition 0.01 --- precondition 0.05 --- variant decrease 0.01 --- precondition 0.01 --- precondition 0.01 --- precondition --- 0.04 precondition --- 1.93 postcondition 0.01 --- postcondition 0.01 --- postcondition 0.01 --- postcondition 0.01 --- postcondition 0.03 --- postcondition 0.01 --- VC for tower_of_hanoi --- --- split_goal_right precondition 0.02 --- precondition 0.01 --- precondition 0.02 --- precondition 0.02 --- postcondition 0.01 --- postcondition 0.02 ---