## White and black balls

A small puzzle from The Correctness Problem in Computer Science (Robert S. Boyer, J. Strother Moore, Academic Prees, 1982).

Auteurs: Jean-Christophe Filliâtre

Catégories: Historical examples / Divisibility

Outils: Why3

see also the index (by topic, by tool, by reference, by year)

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?

Author: Jean-Christophe FilliĆ¢tre (CNRS)

```module WhiteAndBlackBalls

use int.Int
use ref.Ref
use number.Parity

(* 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 ref b = b0 in
let ref w = w0 in
while b + w >= 2 do
invariant { b >= 0 && w >= 0 && b + w >= 1 }
invariant { odd b <-> odd b0 }
variant   { b + w }
let x, y = any (x: int, y: int) ensures {
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
```

# Why3 Proof Results for Project "white_and_black_balls"

## Theory "white_and_black_balls.WhiteAndBlackBalls": fully verified

 Obligations Alt-Ergo 2.0.0 VC for last_is_black 9.30