%------------------------------------------------------------------------------
% 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
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.15Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
