balance.mlw 5.7 KB
Newer Older
1

2
(** {1 Two puzzles involving a Roberval balance}
3

4
   Note: Ghost code is used to get elegant specifications.
5 6

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

10 11
module Roberval

12
  use export int.Int
13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35
  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.
36

37 38 39 40 41 42 43 44 45 46 47 48
    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
49 50
  use import array.Array

51
  (** All values in [balls(lo..hi-1)] are equal to [w], apart from balls[lb]
52 53 54 55 56 57
     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

58 59
  (** Solve the problem for 3 balls, using exactly one weighing.
      The solution [lb] is passed as a ghost argument. *)
60
  let solve3 (balls: array int) (lo: int) (ghost lb: int) (ghost w: int) : int
61
    requires { !counter >= 1 }
62 63
    requires { spec balls lo (lo + 3) lb w }
    ensures  { result = lb }
64
    ensures  { !counter = old !counter - 1 }
65
  =
66 67 68 69 70 71 72 73
    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. *)
74
  let solve8 (balls: array int) (ghost lb: int) (ghost w: int) : int
75
    requires { !counter = 2 }
76 77 78 79
    requires { spec balls 0 8 lb w }
    ensures  { result = lb }
  =
    (* first, compare balls 0,1,2 with balls 3,4,5 *)
80 81 82 83 84 85 86
    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
87 88

end
Léon Gondelman's avatar
Léon Gondelman committed
89

90 91
(** You are given 12 balls, all of the same weight except one
    (for which you don't knwo whether it is lighter or heavier)
Léon Gondelman's avatar
Léon Gondelman committed
92

93 94 95 96
    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.
*)
Léon Gondelman's avatar
Léon Gondelman committed
97

98
module Puzzle12
Léon Gondelman's avatar
Léon Gondelman committed
99

100
  use import Roberval
Léon Gondelman's avatar
Léon Gondelman committed
101 102
  use import array.Array

103 104 105
  (** 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. *)
Léon Gondelman's avatar
Léon Gondelman committed
106
 let solve12 (balls: array int) (ghost w j: int) (ghost b: bool) : (int, bool)
107 108 109 110
    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 }
Léon Gondelman's avatar
Léon Gondelman committed
111 112
    ensures  { result = (j, b) }
 =
113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176
   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
Léon Gondelman's avatar
Léon Gondelman committed
177

178
end