tower_of_hanoi.mlw 3.09 KB
 Andrei Paskevich committed Jan 10, 2013 1 ``````module Hanoi `````` Andrei Paskevich committed Jan 13, 2013 2 `````` (* a simple version where the disks are natural numbers from 1 to n *) `````` Andrei Paskevich committed Jan 10, 2013 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 `````` 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 `````` Andrei Paskevich committed Jan 10, 2013 46 `````` let ghost t = c.rod in `````` Andrei Paskevich committed Jan 10, 2013 47 48 49 50 51 52 53 54 55 56 57 58 59 `````` 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 `````` Jean-Christophe Filliatre committed Dec 21, 2012 60 `````` `````` Andrei Paskevich committed Jan 11, 2013 61 ``````module Tower_of_Hanoi `````` Andrei Paskevich committed Jan 13, 2013 62 `````` (* a generalized version where the disks are arbitrary integers *) `````` Andrei Paskevich committed Jan 11, 2013 63 64 65 66 67 `````` use import int.Int use import list.List use import list.Length `````` Jean-Christophe Filliatre committed Apr 11, 2013 68 `````` use import list.RevAppend `````` Léon Gondelman committed Sep 18, 2014 69 70 `````` clone import list.RevSorted with type t = int, predicate le = (<), goal Transitive.Trans `````` Andrei Paskevich committed Jan 11, 2013 71 72 73 74 `````` type tower = { mutable rod : list int; } invariant { `````` Andrei Paskevich committed Jan 13, 2013 75 `````` Incr.sorted self.rod `````` Andrei Paskevich committed Jan 11, 2013 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 `````` } 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) `````` Andrei Paskevich committed Jan 13, 2013 91 `````` requires { length p = n /\ Decr.sorted p } `````` Andrei Paskevich committed Jan 11, 2013 92 93 94 95 96 97 98 99 100 `````` 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 `````` Andrei Paskevich committed Jan 29, 2013 101 `````` let x,r = match p with Cons x r -> (x,r) | Nil -> absurd end in `````` Andrei Paskevich committed Jan 11, 2013 102 103 104 105 106 107 108 109 110 `````` 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 } `````` Andrei Paskevich committed Jan 13, 2013 111 `````` = hanoi_rec a b c (length a.rod) (ghost rev_append a.rod Nil) Nil `````` Jean-Christophe Filliatre committed Dec 21, 2012 112 113 `````` end``````