white_and_black_balls.mlw 1.33 KB
Newer Older
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18

(* A small puzzle from

   The Correctness Problem in Computer Science
   Robert S. Boyer, J. Strother Moore
   Academic Prees, 1982

   (suggested by Shankar at the Sixth Summer School on Formal Techniques)

   Given a bag containing white and black balls, repeatedly
   - remove a pair from the bag
   - if they are of the same color, insert a white ball
   - if they are of difference colors, insert a black ball
   What is the color of the last ball?
*)

module WhiteAndBlackBalls

19 20 21
  use int.Int
  use ref.Ref
  use number.Parity
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
22 23 24 25 26 27 28 29 30 31 32 33 34 35

  (* answer: the color of the last ball depends on the parity of the
     number of black balls, which is an invariant of the process *)

  let last_is_black (b0 w0: int) : bool
    requires { b0 >= 0 && w0 >= 0 && b0 + w0 >= 1 }
    ensures  { result <-> odd b0 }
  =
    let b = ref b0 in
    let w = ref w0 in
    while !b + !w >= 2 do
      invariant { !b >= 0 && !w >= 0 && !b + !w >= 1 }
      invariant { odd !b <-> odd b0 }
      variant   { !b + !w }
36
      let x, y = any (x: int, y: int) ensures {
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
37 38 39 40 41 42 43 44 45 46 47 48
        0 <= x && 0 <= y && x + y = 2 && x <= !b && y <= !w } in
      if x = 0 || y = 0 then begin (* same color -> insert a white *)
        b := !b - x;
        w := !w - y + 1
      end else begin (* different color -> insert a black *)
        b := !b - x + 1;
        w := !w - y
      end
    done;
    !b > 0

end