balance.mlw 5.65 KB
 Jean-Christophe Filliatre committed Dec 10, 2013 1 `````` `````` Jean-Christophe Filliatre committed Apr 01, 2014 2 ``````(** {1 Two puzzles involving a Roberval balance} `````` Jean-Christophe Filliatre committed Dec 10, 2013 3 `````` `````` Jean-Christophe Filliatre committed Apr 01, 2014 4 `````` Note: Ghost code is used to get elegant specifications. `````` Jean-Christophe Filliatre committed Dec 10, 2013 5 6 `````` Jean-Christophe Filliâtre (CNRS), December 2013 `````` Jean-Christophe Filliatre committed Apr 01, 2014 7 `````` Léon Gondelman (Université Paris-Sud), April 2014 `````` Jean-Christophe Filliatre committed Dec 10, 2013 8 9 ``````*) `````` Jean-Christophe Filliatre committed Apr 01, 2014 10 11 ``````module Roberval `````` Guillaume Melquiond committed Aug 21, 2014 12 `````` use export int.Int `````` Jean-Christophe Filliatre committed Apr 01, 2014 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. `````` Jean-Christophe Filliatre committed Dec 10, 2013 36 `````` `````` Jean-Christophe Filliatre committed Apr 01, 2014 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 `````` Jean-Christophe Filliatre committed Dec 10, 2013 49 50 `````` use import array.Array `````` Guillaume Melquiond committed May 15, 2018 51 `````` (** All values in [balls(lo..hi-1)] are equal to [w], apart from [balls[lb]] `````` Jean-Christophe Filliatre committed Dec 10, 2013 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 `````` Jean-Christophe Filliatre committed Apr 01, 2014 58 59 `````` (** Solve the problem for 3 balls, using exactly one weighing. The solution [lb] is passed as a ghost argument. *) `````` Jean-Christophe Filliatre committed Dec 10, 2013 60 `````` let solve3 (balls: array int) (lo: int) (ghost lb: int) (ghost w: int) : int `````` Jean-Christophe Filliatre committed Apr 01, 2014 61 `````` requires { !counter >= 1 } `````` Jean-Christophe Filliatre committed Dec 10, 2013 62 63 `````` requires { spec balls lo (lo + 3) lb w } ensures { result = lb } `````` Jean-Christophe Filliatre committed Apr 01, 2014 64 `````` ensures { !counter = old !counter - 1 } `````` Jean-Christophe Filliatre committed Dec 10, 2013 65 `````` = `````` Jean-Christophe Filliatre committed Apr 01, 2014 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. *) `````` Jean-Christophe Filliatre committed Dec 10, 2013 74 `````` let solve8 (balls: array int) (ghost lb: int) (ghost w: int) : int `````` Jean-Christophe Filliatre committed Apr 01, 2014 75 `````` requires { !counter = 2 } `````` Jean-Christophe Filliatre committed Dec 10, 2013 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 *) `````` Jean-Christophe Filliatre committed Apr 01, 2014 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 `````` Jean-Christophe Filliatre committed Dec 10, 2013 87 88 `````` end `````` Léon Gondelman committed Apr 01, 2014 89 `````` `````` Jean-Christophe Filliatre committed Apr 01, 2014 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 committed Apr 01, 2014 92 `````` `````` Jean-Christophe Filliatre committed Apr 01, 2014 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 committed Apr 01, 2014 97 `````` `````` Jean-Christophe Filliatre committed Apr 01, 2014 98 ``````module Puzzle12 `````` Léon Gondelman committed Apr 01, 2014 99 `````` `````` Jean-Christophe Filliatre committed Apr 01, 2014 100 `````` use import Roberval `````` Léon Gondelman committed Apr 01, 2014 101 102 `````` use import array.Array `````` Jean-Christophe Filliatre committed Apr 01, 2014 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 committed Apr 01, 2014 106 `````` let solve12 (balls: array int) (ghost w j: int) (ghost b: bool) : (int, bool) `````` Jean-Christophe Filliatre committed Apr 01, 2014 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 committed Apr 01, 2014 111 112 `````` ensures { result = (j, b) } = `````` Jean-Christophe Filliatre committed Apr 01, 2014 113 114 115 116 117 118 `````` 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 `````` Andrei Paskevich committed Jun 11, 2017 119 `````` | Right -> 11, False | _ -> 11, True end `````` Jean-Christophe Filliatre committed Apr 01, 2014 120 121 `````` | Right -> (* 0,8 < 9,10 *) match balance balls[9] balls[10] with `````` Andrei Paskevich committed Jun 11, 2017 122 123 124 `````` | Equal -> 8, True | Right -> 10, False | Left -> 9, False `````` Jean-Christophe Filliatre committed Apr 01, 2014 125 126 127 `````` end | Left -> (* 0,8 > 9,10 *) match balance balls[9] balls[10] with `````` Andrei Paskevich committed Jun 11, 2017 128 129 130 `````` | Equal -> 8, False | Right -> 9, True | Left -> 10, True `````` Jean-Christophe Filliatre committed Apr 01, 2014 131 132 133 134 135 136 137 `````` 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 `````` Andrei Paskevich committed Jun 11, 2017 138 139 140 `````` | Equal -> 3, True | Right -> 7, False | Left -> 6, False `````` Jean-Christophe Filliatre committed Apr 01, 2014 141 142 143 `````` end | Right -> (* 0,1,4 < 2,5,8 *) match balance balls[0] balls[1] with `````` Andrei Paskevich committed Jun 11, 2017 144 145 146 `````` | Equal -> 5, False | Right -> 0, True | Left -> 1, True `````` Jean-Christophe Filliatre committed Apr 01, 2014 147 148 149 `````` end | Left -> (* 0,1,4 > 2,5,8 *) match balance balls[4] balls[8] with `````` Andrei Paskevich committed Jun 11, 2017 150 151 `````` | Equal -> 2, True | _ -> 4, False `````` Jean-Christophe Filliatre committed Apr 01, 2014 152 153 154 155 156 157 158 `````` 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 `````` Andrei Paskevich committed Jun 11, 2017 159 160 161 `````` | Equal -> 3, False | Right -> 6, True | Left -> 7, True `````` Jean-Christophe Filliatre committed Apr 01, 2014 162 163 164 `````` end | Right -> (* 0,1,4 < 2,5,8 *) match balance balls[2] balls[5] with `````` Andrei Paskevich committed Jun 11, 2017 165 166 167 `````` | Equal -> 4, True | Right -> 5, False | Left -> 2, False `````` Jean-Christophe Filliatre committed Apr 01, 2014 168 169 170 `````` end | Left -> (* 0,1,4 > 2,5,8 *) match balance balls[0] balls[1] with `````` Andrei Paskevich committed Jun 11, 2017 171 172 173 `````` | Equal -> 5, True | Right -> 1, False | Left -> 0, False `````` Jean-Christophe Filliatre committed Apr 01, 2014 174 175 176 `````` end end end `````` Léon Gondelman committed Apr 01, 2014 177 `````` `````` Guillaume Melquiond committed Aug 21, 2014 178 ``end``