% W.H. Hesselink, 17th July 2003 (modified 11 September 2004)
% Binary search, see Program Correctness
% Given are constants w: int and max: nat and
% a constant array f: [below[max+1] -> int] with f(0) <= w < f(max).
% To determine a value i: below[max] with f(i) <= w < f(i+1)
%
% We use program variables left, right with the invariant
% (inv) left < right and f(left) <= w < f(right)
% and the guard_while: left + 1 < right
% and the variant function vf: right - left.
% We also need an auxiliary variable mid.
% The total program is
% left := 0 , right := max ;
% while left + 1 < right do
% mid := (left + right) div 2 ;
% if f(mid) <= w then left := mid else right := mid end
% end .
% The result is the final value of left.
binsearch: THEORY
BEGIN
IMPORTING programs, more_floor,
swap % swap is imported only to get it in the dump
% Three given constants
w: real
max: nat
f: [int -> real]
% This function represents the array in which to search.
% Note that it also has values for indices < 0 or > max.
% This is in order to avoid unprovable TCCs
econdition: bool = % Looks like a preconditions, but it is constant!
(f(0) <= w and w < f(max))
state: TYPE = [# left, right, mid: int #] % Note the types!
x: VAR state
postcondition (x): bool =
x`left < max and f(x`left) <= w and w < f(x`left + 1)
% The assignments as commands:
init (x): state = x WITH [`left := 0, `right := max]
body0 (x): state = x WITH [`mid := ndiv (x`left + x`right, 2)]
body1 (x): state = x WITH [`left := x`mid]
body2 (x): state = x WITH [`right := x`mid]
guard_if (x): bool = (f(x`mid) <= w)
guard_while (x): bool = (x`left + 1 < x`right)
body12: command[state] = ifThenElse (guard_if, body1, body2)
body: command[state] = body0 ^ body12
% The loop cannot be a command since, in principle, it need not terminate.
loop: program[state] = while (guard_while, lift (body))
prog: program[state] = lift(init) ^ loop
% We now want to prove correctness (fullset is defined in the prelude):
% econdition IMPLIES tcHoare (fullset[state], prog, postcondition)
inv (x): bool = % the invariant
0 <= x`left and x`right <= max and
x`left < x`right and f(x`left) <= w and w < f(x`right)
post_implied: LEMMA
subset? (inv AND NOT guard_while, postcondition)
inv_initialized: LEMMA
econdition IMPLIES tcHoare (fullset[state], init, inv)
% Auxiliary lemmas for the proof of invariance
m, n: VAR int
b: VAR posnat
inHalfsR: LEMMA % ndiv
m + 1 < n IMPLIES ndiv (m + n, 2) < n
inHalfsL: LEMMA % ndiv
m + 1 < n IMPLIES m < ndiv (m + n, 2)
inv_kept_valid: LEMMA
tcHoare (inv AND guard_while, body, inv)
vf (x): int =
x`right - x`left
vf_is_variant: LEMMA
isVariant (vf, inv, guard_while, body)
loop_correct: LEMMA
tcHoare (inv, loop, postcondition)
correctness: LEMMA
econdition IMPLIES tcHoare (fullset[state], prog, postcondition)
END binsearch