max_array[N: posnat, T: TYPE+, <= : (total_order?[T]) ]: THEORY %------------------------------------------------------------------------ % % max (basic definitions and properties) % ------------------------------------------- % % Author: Ricky W. Butler % % This theory defines the maximum function over an array of values % from an ordered type. This is done in an implementation-independent % manner. However, a recursive executable form is included to % demonstrate that the definition is sound. % % The following functions are defined: % % Imax(A,ii,jj) = general definition of maximum of array A % over the internal range from ii to jj. % Returns the index into the array. % % imax(A) = general definition of maximum of array A. % Returns the index into the array. % % max(A) = general definition of maximum of array A. % Returns the maximal element. % % Notes: % 1. The properties of imax and max are readily obtained via % TYPEPRED "max" and TYPEPRED "imax" or through use of % max_lem and imax_lem. % 2. Since there may be replicates in A, the return type of imax % may not be a singleton set. %------------------------------------------------------------------------ EXPORTING ALL WITH below_arrays[N,T] BEGIN A,A1,A2: VAR ARRAY[below(N) -> T] x: VAR T ii,jj,j: VAR below(N) IMPORTING below_arrays[N,T], max_array_def[N,T,<=] imax(A): {i: below(N)| (FORALL ii: A(ii) <= A(i))} max(A): { t: T | (FORALL ii: A(ii) <= t) AND (EXISTS jj: A(jj) = t)} % LEMMAs that follow immediately from TYPEPRED "imax" and TYPEPRED "max" max_lem : LEMMA A(ii) <= max(A) max_in? : LEMMA in?(max(A),A) imax_lem : LEMMA A(imax(A)) = max(A) max_def : LEMMA (FORALL ii: A(ii) <= max(A)) AND in?(max(A),A) max_it_is : LEMMA (FORALL ii: A(ii) <= x) AND in?(x,A) IMPLIES max(A) = x imax_1 : LEMMA N = 1 IMPLIES imax(A) = 0 max_2 : LEMMA N = 2 IMPLIES max(A) = IF A(0) <= A(1) THEN A(1) ELSE A(0) ENDIF END max_array