| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/fault_tolerance/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 594 B |
|
Quelle ordered_message.pvs Sprache: PVS |
|||||||||
|
%
% % Purpose : a message with a linear order. % % ordered_message[T: TYPE+, leq: (total_order?[T])]: THEORY BEGIN IMPORTING message[T] d1, d2: VAR message valid_iff_ord1: LEMMA (valid?(d1) IFF ord(d1) = 1) d3: VAR message <=(d1, d2): bool = IF valid?(d1) & valid?(d2) THEN leq(value(d1), value(d2)) ELSE ord(d1) <= ord(d2) ENDIF eq_iff: LEMMA d1 = d2 IFF (valid?(d1) AND valid?(d2) AND value(d1) = value(d2)) OR (ord(d1) = ord(d2) AND ord(d1) /= 1 ) message_total_order: JUDGEMENT <= HAS_TYPE (total_order?[message[T]]) END ordered_message ¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28