Wiki Agenda Contact Version française

A small puzzle involving a Roberval balance


Authors: Jean-Christophe Filliâtre / Léon Gondelman

Topics: Ghost code

Tools: Why3

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



Two puzzles involving a Roberval balance

Note: Ghost code is used to get elegant specifications.

Jean-Christophe Filliâtre (CNRS), December 2013 Léon Gondelman (Université Paris-Sud), April 2014

module Roberval

  use export int.Int
  use export ref.Refint

  type outcome = Left | Equal | Right

the side of the heaviest mass i.e. where the balance leans

  val ghost counter: ref int

how many times can we use the balance

  val balance (left right: int) : outcome
    requires { !counter > 0 }
    ensures  { match result with
               | Left  -> left > right
               | Equal -> left = right
               | Right -> left < right
               end }
    writes   { counter }
    ensures  { !counter = old !counter - 1 }

end

You are given 8 balls and a Roberval balance. All balls have the same weight, apart from one, which is lighter. Using the balance at most twice, determine the lighter ball.

Though this problem is not that difficult (though, you may want to think about it before reading any further), it is an interesting exercise in program specification.

The index of the lighter ball is passed as a ghost argument to the program. Thus it cannot be used to compute the answer, but only to write the specification.

module Puzzle8

  use import Roberval
  use import array.Array

All values in balls(lo..hi-1) are equal to w, apart from ballslb which is smaller.

  predicate spec (balls: array int) (lo hi: int) (lb w: int) =
    0 <= lo <= lb < hi <= length balls &&
    (forall i: int. lo <= i < hi -> i <> lb -> balls[i] = w) &&
    balls[lb] < w

Solve the problem for 3 balls, using exactly one weighing. The solution lb is passed as a ghost argument.

  let solve3 (balls: array int) (lo: int) (ghost lb: int) (ghost w: int) : int
    requires { !counter >= 1 }
    requires { spec balls lo (lo + 3) lb w }
    ensures  { result = lb }
    ensures  { !counter = old !counter - 1 }
  =
    match balance balls[lo] balls[lo+1] with
    | Right -> lo
    | Left  -> lo+1
    | Equal -> lo+2
    end

Solve the problem for 8 balls, using exactly two weighings. The solution lb is passed as a ghost argument.

  let solve8 (balls: array int) (ghost lb: int) (ghost w: int) : int
    requires { !counter = 2 }
    requires { spec balls 0 8 lb w }
    ensures  { result = lb }
  =
    (* first, compare balls 0,1,2 with balls 3,4,5 *)
    match balance (balls[0] + balls[1] + balls[2])
                  (balls[3] + balls[4] + balls[5]) with
    | Right -> solve3 balls 0 lb w
    | Left  -> solve3 balls 3 lb w
    (* 0,1,2 = 3,4,5 thus lb must be 6 or 7 *)
    | Equal -> match balance balls[6] balls[7] with Right -> 6 | _ -> 7 end
    end

end

You are given 12 balls, all of the same weight except one (for which you don't knwo whether it is lighter or heavier)

Given a Roberval balance, you have to find the intruder, and determine whether it is lighter or heavier, using the balance at most three times.

module Puzzle12

  use import Roberval
  use import array.Array

The index j of the intruder, its status b (whether it is lighter or heavier), and the weight w of the other balls are all passed as ghost arguments.

 let solve12 (balls: array int) (ghost w j: int) (ghost b: bool) : (int, bool)
    requires { !counter = 3 }
    requires { 0 <= j < 12 = length balls }
    requires { forall i: int. 0 <= i < 12 -> i <> j -> balls[i] = w }
    requires { if b then balls[j] < w else balls[j] > w }
    ensures  { result = (j, b) }
 =
   match balance (balls[0] + balls[1] + balls[2] + balls[3])
                 (balls[4] + balls[5] + balls[6] + balls[7]) with
   | Equal -> (* 0,1,2,3 = 4,5,6,7 *)
      match balance (balls[0] + balls[8]) (balls[9] + balls[10]) with
      | Equal -> (* 0,8 = 9,10 *)
         match balance balls[0] balls[11] with
         | Right -> (11, False) | _ -> (11, True) end
      | Right -> (* 0,8 < 9,10 *)
         match balance balls[9] balls[10] with
         | Equal -> (8, True)
         | Right -> (10,  False)
         | Left  -> (9, False)
         end
      | Left -> (* 0,8 > 9,10 *)
         match balance balls[9] balls[10] with
         | Equal -> (8, False)
         | Right -> (9,  True)
         | Left  -> (10, True)
         end
      end
   | Right -> (* 0,1,2,3 < 4,5,6,7 *)
      match balance (balls[0] + balls[1] + balls[4])
                    (balls[2] + balls[5] + balls[8]) with
      | Equal -> (* 0,1,4 = 2,5,8 *)
         match balance balls[6] balls[7] with
         | Equal -> (3, True)
         | Right -> (7, False)
         | Left -> (6, False)
         end
      | Right -> (* 0,1,4 < 2,5,8 *)
         match balance balls[0] balls[1] with
         | Equal -> (5, False)
         | Right -> (0, True)
         | Left -> (1, True)
         end
      | Left -> (* 0,1,4 > 2,5,8 *)
         match balance balls[4] balls[8] with
         | Equal -> (2, True)
         | _     -> (4, False)
         end
      end
   | Left -> (* 0,1,2,3 > 4,5,6,7 *)
      match balance (balls[0] + balls[1] + balls[4])
                    (balls[2] + balls[5] + balls[8]) with
      | Equal -> (* 0,1,4 = 2,5,8 *)
         match balance balls[6] balls[7] with
         | Equal -> (3, False)
         | Right -> (6, True)
         | Left -> (7, True)
         end
      | Right -> (* 0,1,4 < 2,5,8 *)
         match balance balls[2] balls[5] with
         | Equal -> (4, True)
         | Right -> (5, False)
         | Left -> (2, False)
         end
      | Left -> (* 0,1,4 > 2,5,8 *)
         match balance balls[0] balls[1] with
         | Equal -> (5, True)
         | Right -> (1, False)
         | Left -> (0, False)
         end
      end
    end

end

download ZIP archive