% 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