white_and_black_balls.mlw 1.33 KB
 Jean-Christophe Filliatre committed May 22, 2016 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 `````` Andrei Paskevich committed Jun 15, 2018 19 20 21 `````` use int.Int use ref.Ref use number.Parity `````` Jean-Christophe Filliatre committed May 22, 2016 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 } `````` Andrei Paskevich committed Jun 07, 2018 36 `````` let x, y = any (x: int, y: int) ensures { `````` Jean-Christophe Filliatre committed May 22, 2016 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``````