Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
142aeef2
Commit
142aeef2
authored
Apr 01, 2014
by
Jean-Christophe Filliâtre
Browse files
[gallery] cleaning up balance.mlw
parent
24fc5f16
Changes
2
Expand all
Hide whitespace changes
Inline
Side-by-side
examples/balance.mlw
View file @
142aeef2
(* 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.
(** {1 Two puzzles involving a Roberval balance}
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.
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 Balance
module Roberval
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.
use import int.Int
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
[
are equal to [w], apart from balls[lb]
(*
*
All values in
[
balls
(
lo..hi
-1)]
are equal to [w], apart from balls[lb]
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 *)
(** 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 }
=
if balls[lo] < balls[lo+1] then lo
else if balls[lo] > balls[lo+1] then lo+1
else lo+2
(* Solve the problem for 8 balls, using exactly two weighings *)
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 *)
if balls[0] + balls[1] + balls[2] <
balls[
3
] + balls[
4
] + balls[
5] then
solve3 balls 0 lb w
else if balls[0] + balls[1] + balls[2] > balls[3] + balls[4] + balls[5] then
solve3 balls 3 lb w
else
(* 0,1,2 = 3,4,5 thus lb must be 6 or 7 *)
if balls[6] < balls[7] then 6 else 7
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
Balanc
e12
module
Puzzl
e12
use import
int.Int
use import
Roberval
use import array.Array
(* All values in balls[lo..hi[ are equal to [w], apart from balls[lb]
which is of a different weight (lighter or heavier) . *)
predicate spec (balls: array int) (lo hi j: int) (w: int) (b: bool) =
0 <= lo <= j < hi <= length balls &&
(forall i: int. lo <= i < hi -> i <> j -> balls[i] = w) &&
(if b then balls[j] < w else balls[j] > w)
(* j : the index of the different ball,
b : the status (lighter or heavier) of the different ball
False True meaning heavier and True meaining lighter *)
(** 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 { spec balls 0 12 j w b }
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) }
=
if balls[0] + balls[1] + balls[2] + balls[3] =
balls[4] + balls[5] + balls[6] + balls[7]
then
if balls[0] + balls[8] = balls[9] + balls[10]
then
if balls[0] < balls[11]
then (11, False)
else (11, True)
else if balls[0] + balls[8] < balls[9] + balls[10]
then
if balls[9] = balls[10] then (8, True)
else if balls[9] < balls[10] then (10, False) else (9, False)
else
if balls[9] = balls[10] then (8, False)
else if balls[9] < balls[10] then (9, True) else (10, True)
else if balls[0] + balls[1] + balls[2] + balls[3] <
balls[4] + balls[5] + balls[6] + balls[7]
then
if balls[0] + balls[1] + balls[4] = balls[2] + balls[5] + balls[8]
then
if balls[6] = balls[7] then (3, True)
else if balls[6] < balls[7] then (7, False) else (6, False)
else if balls[0] + balls[1] + balls[4] < balls[2] + balls[5] + balls[8]
then
if balls[0] = balls[1] then (5, False)
else if balls[0] < balls[1] then (0, True) else (1, True)
else
if balls[4] = balls[8] then (2, True) else (4, False)
else
if balls[0] + balls[1] + balls[4] = balls[2] + balls[5] + balls[8]
then
if balls[6] = balls[7] then (3, False)
else if balls[6] < balls[7] then (6, True) else (7, True)
else if balls[0] + balls[1] + balls[4] < balls[2] + balls[5] + balls[8]
then
if balls[2] = balls[5] then (4, True )
else if balls[2] < balls[5] then (5, False) else (2, False)
else
if balls[0] = balls[1] then (5, True) else
if balls[0] < balls[1] then (1, False) else (0, False)
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
\ No newline at end of file
examples/balance/why3session.xml
View file @
142aeef2
This diff is collapsed.
Click to expand it.
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment