Quelle  middle_value_select.pvs

%------------------------------------------------------------------------------
% Lee Pike 
% lee.s.pike@nasa.gov
% Formal Methods Group, NASA Langley Research Center
%
% PVS Version 3.1
%
% PURPOSE: 
% To model a middle-value selection over bags.
%------------------------------------------------------------------------------

middle_value_select[T: NONEMPTY_TYPE, 
                  leq: (total_order?[T])]: THEORY

BEGIN 

  IMPORTING bag_filters[T, leq]

  A                 : VAR finite_bag
  i, v              : VAR T  

  mid_val?(A)(v)    : bool = 2 * card(l_filter(A, v)) > card(A) AND
                             2 * card(u_filter(A, v)) >= card(A) 

  mid_val(A)        : T = epsilon(mid_val?(A))

  mid_val_singleton : LEMMA NOT empty?(A) IMPLIES singleton?(mid_val?(A))

END middle_value_select