% -------------------------------------------------------------------
%
% Verification of linear search algorithm.
%
% -------------------------------------------------------------------

newcontext "linsearch";

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

% the types
INDEX: TYPE = NAT;
ELEM:  TYPE;
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;
x: ELEM;
oldx: ELEM;
i: NAT;
n: NAT;
r: INT;

Input: BOOLEAN =
  olda = a AND oldx = x AND n = length(a) AND i = 0 AND r = -1;

Output: BOOLEAN =
  a = olda 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 AND
     (FORALL(j:NAT): j < r => get(a,j) /= x)));

Invariant: (ARR, ELEM, NAT, NAT, INT) -> BOOLEAN =
  LAMBDA(a: ARR, x: ELEM, i: NAT, n: NAT, r: INT):
    olda = a AND oldx = x AND n = length(a) AND i <= n AND
    (FORALL(j:NAT): j < i => get(a,j) /= x) AND
    (r = -1 OR (r = i AND i < n AND get(a,r) = x));
    
A: FORMULA
  Input => Invariant(a, x, i, n, r);

B1: FORMULA
  Invariant(a, x, i, n, r) AND i < n AND r = -1 AND get(a,i) = x 
    => Invariant(a,x,i,n,i);

B2: FORMULA
  Invariant(a, x, i, n, r) AND i < n AND r = -1 AND get(a,i) /= x 
    => Invariant(a,x,i+1,n,r);

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