% -------------------------------------------------------------------
%
% Verification of maximum search algorithm.
%
% -------------------------------------------------------------------

newcontext "insert";

% -------------------------------------------------------------------
% 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;

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

a: ARR; olda: ARR;
n: NAT; oldn: NAT;
p: NAT; oldp: NAT;
x: NAT; oldx: NAT;
i: NAT; 
b: ARR;

Input: BOOLEAN =
  a = olda AND n = oldn AND p = oldp AND x = oldx AND p < n AND i = 0 AND
  n = length(a) AND n+1 = length(b);

Output: BOOLEAN =
  a = olda AND n = oldn AND p = oldp AND x = oldx AND 
  n+1 = length(b) AND
  (FORALL(j:NAT): j < p => get(a, j) = get(b, j)) AND
  x = get(b, p) AND
  (FORALL(j:NAT): p <= j AND j < n => get(a, j) = get(b, j+1));

Invariant: (ARR, NAT, NAT, NAT, NAT, ARR) -> BOOLEAN =
  LAMBDA(a:ARR, n:NAT, p:NAT, x:NAT, i:NAT, b: ARR):
    a = olda AND n = oldn AND p = oldp AND x = oldx AND
    p < n AND i <= n+1 AND
    n = length(a) AND n+1 = length(b) AND
    (FORALL(j:NAT): j < i => 
       (j < p => get(b, j) = get(a, j)) AND
       (j = p => get(b, j) = x) AND
       (j > p => get(b, j) = get(a, j-1)));
    
A: FORMULA
  Input => Invariant(a, n, p, x, i, b);

B1: FORMULA
  Invariant(a, n, p, x, i, b) AND i < n+1 AND i < p =>
  Invariant(a, n, p, x, i+1, put(b, i, get(a, i)));

B2: FORMULA
  Invariant(a, n, p, x, i, b) AND i < n+1 AND NOT i < p AND i = p =>
  Invariant(a, n, p, x, i+1, put(b, i, x));

B3: FORMULA
  Invariant(a, n, p, x, i, b) AND i < n+1 AND NOT i < p AND NOT i = p =>
  Invariant(a, n, p, x, i+1, put(b, i, get(a, i-1)));

C: FORMULA
  Invariant(a, n, p, x, i, b) AND NOT i < n+1 => Output;