Quelle  fault_masking_vote.pvs

%------------------------------------------------------------------------------
% Lee Pike 
% lee.s.pike@nasa.gov
% 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