%------------------------------------------------------------------------------
% Lee Pike
% [email protected]
% 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
¤ Dauer der Verarbeitung: 0.1 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.
|
