Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
majority_vote.pvs
Sprache: Unknown
%------------------------------------------------------------------------------
% 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.7 Sekunden
(vorverarbeitet)
]
|
|
