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: VARARRAY[below(N) -> T]
x: VAR T
ii,jj,j: VAR below(N)
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
