%------------------------------------------------------------------------------
% Lee Pike
% [email protected]
% Formal Methods Group, NASA Langley Research Center
%
% PVS Version 3.1
%
% PURPOSE:
% To model a majority vote over bags.
%------------------------------------------------------------------------------
majority_vote[T: NONEMPTY_TYPE]: THEORY
BEGIN
IMPORTING finite_bags[T]
A : VAR finite_bag
i, v : VAR T
no_majority : T
maj?(A)(v) : bool = 2 * A(v) > card(A)
maj(A) : T = IF empty?(maj?(A))
THEN no_majority
ELSE epsilon(maj?(A)) ENDIF
maj_size : LEMMA 2 * A(v) > card(A) IMPLIES
2 * card(purge(v, A)) < card(A)
maj_single_or_empty: LEMMA singleton?(maj?(A)) OR empty?(maj?(A))
maj_unique : LEMMA maj?(A)(v) IMPLIES maj(A) = v
maj_pigeonhole : LEMMA maj?(A)(v) AND maj?(A)(i) IMPLIES v = i
maj_is_extraction : LEMMA maj?(A)(v) IMPLIES
maj?(A) = bag_to_set(extract(v, A))
END majority_vote
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤
|
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.
|
