% -------------------------------------------------------------------
%
% Verification of binary search algorithm.
%
% -------------------------------------------------------------------

newcontext "binarysearch";

% -------------------------------------------------------------------
% the constructive definition of arrays.
% -------------------------------------------------------------------

% the types
INDEX: TYPE = NAT;
ELEM:  TYPE = INT;
ARR:   TYPE = [INDEX, ARRAY INDEX OF ELEM];

% error constants
any:      ARRAY INDEX OF ELEM;
anyelem:  ELEM;
anyarray: ARR;

% a selector operation
content: ARR -> (ARRAY INDEX OF ELEM) = LAMBDA(a:ARR): a.1;

% the definitions
length: ARR -> INDEX = 
  LAMBDA(a:ARR): a.0;
new: INDEX -> ARR = 
  LAMBDA(n:INDEX): (n, any);
put: (ARR, INDEX, ELEM) -> ARR =
 LAMBDA(a:ARR, i:INDEX, e:ELEM):
   IF i < length(a) 
     THEN (length(a), content(a) WITH [i]:=e)
     ELSE anyarray
   ENDIF;
get: (ARR, INDEX) -> ELEM =
  LAMBDA(a:ARR, i:INDEX):
    IF i < length(a) THEN content(a)[i] ELSE anyelem ENDIF;

% -------------------------------------------------------------------
% truncation arithmetic
% -------------------------------------------------------------------

floor: REAL->INT;

floorAxiom: AXIOM
  FORALL(x:REAL):
    floor(x) <= x AND NOT(EXISTS(y:INT): y <= x AND floor(x) < y);

% -------------------------------------------------------------------
% the verification conditions
% -------------------------------------------------------------------

a: ARR;
olda: ARR;
x: INT;
oldx: INT;
low: INT;
high: INT;
mid: INT;
r: INT;

Input: BOOLEAN =
  olda = a AND oldx = x AND r = -1 AND low = 0 AND high = length(a)-1 AND
  (FORALL (j:NAT): j < length(a)-1 => get(a, j) <= get(a, j+1));

Output: BOOLEAN =
  a = olda AND x = oldx AND
  ((r = -1 AND 
     (FORALL(j:NAT): j < length(a) => get(a,j) /= x)) OR
   (0 <= r AND r < length(a) AND get(a,r) = x));

Invariant: (ARR, INT, INT, INT, INT) -> BOOLEAN =
  LAMBDA(a: ARR, x: INT, low: INT, high: INT, r: INT):
    a = olda AND x = oldx AND
    (FORALL (j:NAT): j < length(a)-1 => get(a, j) <= get(a, j+1)) AND
      -1 <= r AND r < length(a) AND
      (r /= -1 => get(a, r) = x) AND
      0 <= low AND low <= length(a) AND 
      -1 <= high AND high < length(a) AND
      low <= high+1 AND
      (FORALL (j:NAT): j < low AND j < length(a) => get(a,j) < x) AND
      (FORALL (j:NAT): high < j AND j < length(a) => get(a,j) > x);

L: FORMULA
  (FORALL (j:NAT): j < length(a)-1 => get(a, j) <= get(a, j+1)) => 
    (FORALL (j, k:NAT): j < length(a) AND k < length(a) AND k <= j => 
      get(a, k) <= get(a, j));

A: FORMULA
  Input 
  => Invariant(a, x, low, high, r);

B1: FORMULA
  Invariant(a, x, low, high, r) AND r = -1 AND low <= high AND
  get(a, floor((low+high)/2)) = x
  => Invariant(a, x, low, high, floor((low+high)/2));

B2: FORMULA
  Invariant(a, x, low, high, r) AND r = -1 AND low <= high AND
  NOT get(a, floor((low+high)/2)) = x AND get(a, floor((low+high)/2)) < x
  => Invariant(a, x, floor((low+high)/2)+1, high, r);

B3: FORMULA
  Invariant(a, x, low, high, r) AND r = -1 AND low <= high AND
  get(a, floor((low+high)/2)) /= x AND NOT get(a, floor((low+high)/2)) < x
  => Invariant(a, x, low, floor((low+high)/2)-1, r);

C: FORMULA
  Invariant(a, x, low, high, r) AND NOT(r = -1 AND low <= high) 
  => Output;