SSL min_seq.pvs   Sprache: unbekannt

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%

[ Verzeichnis aufwärts0.28unsichere Verbindung  Übersetzung europäischer Sprachen durch Browser  ]