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 import int.Int
  use import list.List
  use import list.Length
  use import list.SortedInt

  type tower = {
    mutable rod : list int;
  } invariant {
    sorted self.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 import int.Int
  use import list.List
  use import list.Length

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

  type tower = {
    mutable rod : list int;
  } invariant {
    Incr.sorted self.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 in 16.71 s

ObligationsAlt-Ergo (0.99.1)CVC3 (2.4.1)CVC4 (1.4)Eprover (1.8-001)Spass (3.7)Vampire (0.6)
VC for move0.05------0.010.170.02
VC for hanoi_rec------------------
split_goal_wp
  1. variant decrease0.01---0.020.210.530.67
2. precondition0.01---0.020.000.020.02
3. precondition0.04------0.040.221.12
4. precondition0.10------0.050.131.34
5. precondition0.01---0.010.000.020.00
6. precondition0.03------0.010.030.00
7. variant decrease0.01---0.010.250.551.24
8. precondition0.02---0.010.000.030.00
9. precondition0.10------1.791.981.00
10. precondition---0.06---2.74---1.42
11. postcondition0.02---0.020.020.020.00
12. postcondition0.02---0.010.040.020.08
13. postcondition0.01---0.000.010.030.00
14. postcondition0.01---0.000.020.030.01
15. postcondition0.01---0.010.020.020.01
VC for tower_of_hanoi0.08---0.010.010.030.02

Theory "tower_of_hanoi.Tower_of_Hanoi": fully verified in 17.25 s

ObligationsAlt-Ergo (0.95.2)Alt-Ergo (0.99.1)CVC3 (2.4.1)CVC4 (1.4)Eprover (1.8-001)Spass (3.7)Vampire (0.6)Z3 (4.3.1)
RevSorted.Transitive.Trans0.01---------------------
VC for move---0.080.03---0.02---0.04---
VC for hanoi_rec------------------------
split_goal_wp
  1. variant decrease---0.040.020.010.660.671.150.00
2. precondition---0.030.00---0.330.630.43---
3. precondition---0.020.020.010.142.630.02---
4. precondition------0.14---0.050.220.03---
5. precondition------0.15---0.00---0.04---
6. precondition---0.020.030.010.050.050.010.03
7. precondition------0.03---0.000.160.02---
8. variant decrease---0.020.030.010.06---2.410.03
9. precondition---0.010.020.010.060.040.000.02
10. precondition---0.020.020.010.000.040.000.03
11. precondition------0.25---0.000.200.05---
12. precondition------0.24---0.36---1.80---
13. postcondition---0.020.020.010.000.040.000.03
14. postcondition---0.020.35---0.230.750.490.05
15. postcondition---0.010.020.020.000.050.000.03
16. unreachable point---0.010.010.01---------0.03
17. postcondition---0.05---0.030.040.060.00---
18. postcondition---0.04---0.020.030.060.01---
VC for tower_of_hanoi------------------------
split_goal_wp
  1. precondition---0.030.020.030.020.030.010.05
2. precondition---0.010.120.020.020.060.000.03
3. precondition---0.020.030.010.010.030.000.03
4. precondition---0.010.020.010.010.030.000.03
5. postcondition---0.020.020.010.000.030.000.03
6. postcondition---0.020.030.010.010.030.010.03