Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 

products/Sources/formale Sprachen/PVS/structures/   (Beweissystem der NASA Version 6.0.9©)  Datei vom 28.9.2014 mit Größe 3 kB image not shown  

Quellcode-Bibliothek majority_fseq.pvs   Sprache: PVS

 
majority_fseq[T: NONEMPTY_TYPE]: THEORY
%------------------------------------------------------------------------
%
%  majority (basic definitions and properties)
%  -------------------------------------------
%
%      Author: Ricky W. Butler
%
%  This theory defines the majority function over a finite sequence of
%  values.  The following functions are defined:
%           
%           is_majority(mv,fs) -- predicate that is true IFF mv is
%                                 the majority value of the sequence
%
%           maj_exists(fs)     -- predicate that us true IFF a majority
%                                 exists
%
%           maj(fs)            -- function that returns the majority value
%                                 if a majority exists.  If a majority does
%                                 not exist, the function returns an
%                                 unspecified value from the type T.
%                                 This value may not be in the sequence.
%
%           inseq(x,fs)        -- predicate that is true IFF x is in
%                                 the sequence
%
%   Note: the following function can be defined that will return
%   a value from the sequence if a majority does not exist.
%
%     finseq: TYPE = {fs | length(fs) > 0}
%
%     fsq: VAR finseq
%     Maj(fsq): {x: T | in_seq(x,fsq)} = IF maj_exists(fsq) THEN maj(fsq)
%                                        ELSE choose({x: T | in_seq(x,fsq)})
%                                        ENDIF 
%
%------------------------------------------------------------------------

BEGIN

  IMPORTING finite_sets@finite_sets_below
  IMPORTING fseqs[T]

  fs: VAR fsq[T]
  mv, mv1, mv2, x: VAR T

  is_majority(mv: T, fs): bool = 
       2*card({i: below(length(fs)) | seq(fs)(i) = mv}) > length(fs) 

  maj_exists(fs): bool = (EXISTS (mv: T): is_majority(mv,fs))

  maj(fs): {mv | maj_exists(fs) => is_majority(mv,fs)}

  in_seq(x,fs): bool = (EXISTS (i: below(length(fs))): seq(fs)(i) = x)

  is_majority_unique: LEMMA is_majority(mv1,fs) AND is_majority(mv2,fs)
                            IMPLIES mv1 = mv2

  maj_lem:            LEMMA is_majority(mv,fs) IFF 
                            maj_exists(fs) AND maj(fs) = mv

  maj_subset:         LEMMA   (EXISTS (A: finite_set[below(length(fs))]):
                               2*card(A) > length(fs)
                               AND (FORALL (i: below(length(fs))): A(i) 
                                              IMPLIES seq(fs)(i) = mv))
                            IMPLIES is_majority(mv,fs)

  maj_in_seq:         LEMMA is_majority(mv,fs) IMPLIES in_seq(mv,fs)

% ===================== Some Special Sequences ===================

  f1: VAR [below[1] -> T]


  n: VAR posnat
  c: VAR T

  length_eq_1: LEMMA maj(fseq1(c)) = c 

  constant_seq(n,c): fsq[T] = (# length := n,
                                  seq := (LAMBDA (i: nat): c) #)

  is_majority_const: LEMMA is_majority(c, constant_seq(n,c))
  
  maj_const:         LEMMA maj_exists(constant_seq(n,c)) AND
                           maj(constant_seq(n,c)) = c

END majority_fseq

88%


¤ 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.0.22Bemerkung:  (vorverarbeitet)  ¤

*© Formatika GbR, Deutschland




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.