| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/structures/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 786 B |
|
Quelle fault_masking_vote.pvs Sprache: 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 ¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28