Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: trig_values.pvs Sprache: PVS

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

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