Quelle min_seq.pvs Sprache: PVS

min_seq[T: TYPE+, <= : (total_order?[T]) ]: THEORY
%------------------------------------------------------------------------
%
%  min_seq (basic definitions and properties)
%  -------------------------------------------
%
%      Author: Ricky W. Butler
%
%  This theory defines the minimum function over a sequence of values
%  from an ordered type. This is done in an implementation-independent
%  manner.
%
%      Imin(s,ii,jj)     = general definition of minimum of sequence s
%                          over the internal from ii to jj.  Returns the
%                          index into the sequence.
%
%      imin(s)           = general definition of minimum of sequence s.
%                          Returns the index into the sequence.
%
%      min(s)            = general definition of minimum of sequence s.
%                          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_seq_lem and imin_seq_lem.
%     2. Since there may be replicates in s, the return type of imin
%        may not be a singleton set.
%------------------------------------------------------------------------

  EXPORTING ALL WITH seqs[T]

BEGIN

  IMPORTING seqs[T]

%  seqs: TYPE = {s: finite_sequence[T]  | length(s) > 0}
%  in?(x,s): bool = (EXISTS (ii: dom(s)): x = seq(s)(ii))

  ii,j: VAR nat
  s: VAR ne_seqs
  x: VAR T

  IMPORTING min_array_def

  dom(s): TYPE = below(length(s))
  abv(ii,s): TYPE = {i: nat | ii <= i AND i < length(s)}

  Imin(s, (ii: dom(s)),(jj: abv(ii,s))):
       {i: subrange(ii,jj) | (FORALL j: ii <= j AND j <= jj
                                     IMPLIES seq(s)(i) <= seq(s)(j))}

  Imin_seq_1: LEMMA (FORALL (s: ne_seqs,ii: dom(s)): Imin(s,ii,ii) = ii)

  imin(s): {i: dom(s)| (FORALL (ii: dom(s)): seq(s)(i) <= seq(s)(ii))}

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

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

  min_seq_lem   : LEMMA (FORALL (ii: dom(s)): min(s) <= seq(s)(ii))

  min_seq_in?   : LEMMA in?(min(s),s)

  min_seq_def   : LEMMA FORALL (ii: dom(s)): min(s) <= seq(s)(ii)
                        AND in?(min(s),s)

  min_seq_it_is : LEMMA (FORALL (ii: dom(s)): x <= seq(s)(ii)) AND in?(x,s)
                        IMPLIES min(s) = x

  imin_seq_lem  : LEMMA seq(s)(imin(s)) = min(s)

  imin_seq_1    : LEMMA length(s) = 1 IMPLIES imin(s) = 0

  min_seq_2     : LEMMA length(s) = 2 IMPLIES min(s) =
                    IF seq(s)(0) <= seq(s)(1) THEN seq(s)(0)
                    ELSE seq(s)(1) ENDIF

END min_seq

quality98%

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