|
%
%
% 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.16 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.
|
