Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: max_array.pvs Sprache: PVS

Original von: 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

¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.