Wiki Agenda Contact Version française

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

ObligationsAlt-Ergo 2.0.0
VC tower0.00
VC move---
split_goal_right
VC move.00.01
VC move.10.02
VC move.20.01
VC move.30.01
VC move.40.00
VC hanoi_rec---
split_goal_right
VC hanoi_rec.00.00
VC hanoi_rec.10.01
VC hanoi_rec.20.02
VC hanoi_rec.30.01
VC hanoi_rec.40.00
VC hanoi_rec.50.01
VC hanoi_rec.60.00
VC hanoi_rec.70.00
VC hanoi_rec.80.01
VC hanoi_rec.90.88
VC hanoi_rec.100.01
VC hanoi_rec.110.01
VC hanoi_rec.120.01
VC hanoi_rec.130.00
VC hanoi_rec.140.00
VC hanoi_rec.150.00
VC tower_of_hanoi---
split_goal_right
VC tower_of_hanoi.00.00
VC tower_of_hanoi.10.01
VC tower_of_hanoi.20.00
VC tower_of_hanoi.30.00
VC tower_of_hanoi.40.00

Theory "tower_of_hanoi.Tower_of_Hanoi": fully verified

ObligationsAlt-Ergo 2.0.0
RevSorted.Transitive.Trans0.00
VC tower0.00
VC move---
split_goal_right
VC move.00.01
VC move.10.03
VC move.20.01
VC move.30.02
VC move.40.01
VC hanoi_rec---
split_goal_right
VC hanoi_rec.00.01
VC hanoi_rec.10.01
VC hanoi_rec.20.01
VC hanoi_rec.30.01
VC hanoi_rec.44.87
VC hanoi_rec.54.88
VC hanoi_rec.60.01
VC hanoi_rec.70.05
VC hanoi_rec.80.01
VC hanoi_rec.90.02
VC hanoi_rec.100.01
VC hanoi_rec.110.05
VC hanoi_rec.129.41
VC hanoi_rec.130.01
VC hanoi_rec.140.01
VC hanoi_rec.150.01
VC hanoi_rec.160.01
VC hanoi_rec.170.03
VC hanoi_rec.180.01
VC tower_of_hanoi---
split_goal_right
VC tower_of_hanoi.00.02
VC tower_of_hanoi.10.01
VC tower_of_hanoi.20.02
VC tower_of_hanoi.30.02
VC tower_of_hanoi.40.02
VC tower_of_hanoi.50.01