Quelle min_array.pvs Sprache: PVS

min_array[N: posnat, T: TYPE, <= : (total_order?[T]) ]: THEORY
%------------------------------------------------------------------------
%
%  min (basic definitions and properties)
%  -------------------------------------------
%
%      Author: Ricky W. Butler
%
%  This theory defines the minimum function over an array of values
%  from an ordered type. This is done in an implementation-independent
%  manner.
%
%      Imin(A,ii,jj)     = general definition of minimum of array A
%                          over the internal from ii to jj.  Returns the
%                          index into the array.
%
%      imin(A)           = general definition of minimum of array A.
%                          Returns the index into the array.
%
%      min(A)            = general definition of minimum of array A.
%                          Returns the minimal element.
%
%  Notes:
%     1. The properties of imin and min are readily obtained via
%        TYPEPRED "min" and TYPEPRED "imin" or through use of
%        min_lem and imin_lem.
%     2. Since there may be replicates in A, the return type of imin
%        may not be a singleton set.
%
%------------------------------------------------------------------------

  EXPORTING ALL WITH below_arrays[N,T]

BEGIN

  IMPORTING min_array_def[N,T,<=], below_arrays[N,T]

  A: VAR ARRAY[below(N) -> T]
  x: VAR T
  ii,jj: VAR below(N)

  imin(A): {i: below(N)| (FORALL ii: A(i) <= A(ii))}

  min(A): { t: T | (FORALL ii: t <= A(ii)) AND
                    (EXISTS jj: A(jj) = t)}

% LEMMAs that follow immediately from TYPEPRED "imin" and TYPEPRED "min"

  min_lem   : LEMMA min(A) <= A(ii)

  min_in?   : LEMMA in?(min(A),A)

  min_def   : LEMMA (FORALL ii: min(A) <= A(ii)) AND in?(min(A),A)

  min_it_is : LEMMA (FORALL ii: x <= A(ii)) AND in?(x,A) IMPLIES
                        min(A) = x

  imin_lem  : LEMMA A(imin(A)) = min(A)

  imin_1    : LEMMA N = 1 IMPLIES imin(A) = 0

  min_2     : LEMMA N = 2 IMPLIES min(A) = IF A(0) <= A(1) THEN A(0)
                                           ELSE A(1) ENDIF

END min_array

quality93%

¤ Dauer der Verarbeitung: 0.1 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.