%------------------------------------------------------------------------------
% Lee Pike
% [email protected]
% Formal Methods Group, NASA Langley Research Center
%
% PVS Version 3.1
%
% PURPOSE:
% To prove the equivalence of a majority vote and a middle value
% selection over a bag in the case that a majority value exists.
%------------------------------------------------------------------------------
fault_masking_vote[T: NONEMPTY_TYPE,
leq: (total_order?[T])]: THEORY
BEGIN
IMPORTING majority_vote[T],
middle_value_select[T, leq]
A : VAR finite_bag
IMPORTING bag_filters[T,leq] %% RWB
mid_val_is_maj : LEMMA maj(A) /= no_majority IMPLIES
mid_val(A) = maj(A)
END fault_masking_vote
¤ Dauer der Verarbeitung: 0.2 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.
|
