examples/unraveling_a_card_trick.mlw

   1
   2 (*
   3   Unraveling a Card Trick
   4   Tony Hoare and Natarajan Shankar
   5   Time for Verification
   6   Lecture Notes in Computer Science, 2010, Volume 6200/2010, 195-201,
   7   DOI: 10.1007/978-3-642-13754-9_10
   8   http://www.springerlink.com/content/gn18673357154448/
   9 *)
  10
  11 theory GilbreathCardTrickPure
  12
  13   use export int.Int
  14   use option.Option
  15   use export list.List
  16   use export list.Length
  17   use export list.Append
  18   use export list.Reverse
  19   use list.Nth
  20
  21   constant m: int
  22   axiom m_positive: 0 < m
  23
  24   constant n: int
  25   axiom n_nonnegative: 0 <= n
  26
  27   (* c is a riffle shuffle of a and b *)
  28   inductive shuffle (a b c: list 'a) =
  29   | Shuffle_nil_left:
  30       forall l: list 'a. shuffle l Nil l
  31   | Shuffle_nil_right:
  32       forall l: list 'a. shuffle Nil l l
  33   | Shuffle_cons_left:
  34       forall x: 'a, a b c: list 'a.
  35       shuffle a b c -> shuffle (Cons x a) b (Cons x c)
  36   | Shuffle_cons_right:
  37       forall x: 'a, a b c: list 'a.
  38       shuffle a b c -> shuffle a (Cons x b) (Cons x c)
  39
  40   lemma shuffle_nil_nil_nil: shuffle Nil Nil (Nil: list 'a)
  41
  42   lemma shuffle_sym:
  43      forall a b c: list 'a. shuffle a b c -> shuffle b a c
  44
  45   lemma shuffle_length:
  46     forall a b c: list 'a. shuffle a b c -> length a + length b = length c
  47
  48   (* the list l is composed of n blocks, each being 0,1,...,m-1 *)
  49   predicate suit_ordered (l: list int) =
  50     forall i j: int. 0 <= i < n -> 0 <= j < m -> nth (i * m + j) l = Some j
  51
  52   (* the list l is a sequence of n blocks,
  53      each being a permutation of 0,1,...,m-1 *)
  54   predicate suit_sorted (l: list int) =
  55     (forall i v: int. nth i l = Some v -> 0 <= v < m) /\
  56     (forall i j1 j2: int. 0 <= i < n -> 0 <= j1 < m -> 0 <= j2 < m ->
  57      nth (i * m + j1) l <> nth (i * m + j2) l)
  58
  59   (* TODO: prove it! *)
  60   axiom gilbreath_card_trick:
  61     forall a: list int. length a = n * m -> suit_ordered a ->
  62     forall c d: list int. a = c ++ d ->
  63     forall b: list int. shuffle c (reverse d) b -> suit_sorted b
  64
  65 end
  66
  67 (* a program implementing the card trick using stacks *)
  68 module GilbreathCardTrick
  69
  70   use GilbreathCardTrickPure
  71   use stack.Stack
  72
  73   let shuffle (a b: t int)
  74     ensures { a.elts = Nil /\ b.elts = Nil /\
  75       shuffle (reverse (old a.elts)) (reverse (old b.elts)) result.elts }
  76   = let c = create () in
  77     let ghost a' = create () in
  78     let ghost b' = create () in
  79     while not (is_empty a && is_empty b) do
  80       invariant { reverse (old a.elts) = reverse a.elts ++ a'.elts }
  81       invariant { reverse (old b.elts) = reverse b.elts ++ b'.elts }
  82       invariant { shuffle a'.elts b'.elts c.elts }
  83       variant   { length a + length b }
  84       if not (is_empty a) && (is_empty b || any bool) then begin
  85         ghost (push (safe_top a) a');
  86         push (safe_pop a) c
  87       end else begin
  88         ghost (push (safe_top b) b');
  89         push (safe_pop b) c
  90       end
  91     done;
  92     c
  93
  94   let card_trick (a: t int)
  95     requires { length a = n*m /\ suit_ordered a.elts }
  96     ensures { length result = n*m && suit_sorted result.elts }
  97   = (* cut a into c;d and reverse d in d_ *)
  98     let d_ = create () in
  99     let cut = any int ensures { 0 <= result <= n*m } in
 100     for i = 1 to cut do
 101       invariant { length a = n*m-i+1 /\ length d_ = i-1 /\
 102                   old a.elts = reverse d_.elts ++ a.elts }
 103       push (safe_pop a) d_
 104     done;
 105     assert { old a.elts = reverse d_.elts ++ a.elts };
 106     (* then suffle c (that is a) and d_ to get b *)
 107     shuffle a d_
 108
 109 end