|
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
¤ Dauer der Verarbeitung: 0.21 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
|
