## 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
```