## Towers of Hanoi

Classical recursive algorithm

**Authors:** Andrei Paskevich

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

download ZIP archive

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