Quelle  majority_vote.pvs

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