Quelle max_array.pvs Sprache: PVS

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

quality78%

¤ Dauer der Verarbeitung: 0.35 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.