%------------------------------------------------------------------------- % % "Stronger" and "weaker" orders. Given two relations on T, rel1 and % rel2, if strict_subset?(rel1, rel2), then we say that rel1 is % weaker than rel2, and that rel2 is stronger than rel1. If % subset?(rel1, rel2), then rel1 is weaker than or equal to rel2, and % rel2 is stronger than or equal to rel1. % % For PVS version 3.2. January 14, 2005 % --------------------------------------------------------------------- % Author: Jerry James (jamesj@acm.org), University of Kansas % % EXPORTS % ------- % orders: order_strength[T] % %-------------------------------------------------------------------------
order_strength[T: TYPE]: THEORY BEGIN
t1, t2: VAR T
ord1, ord2: VAR pred[[T, T]]
% Stronger orders: if ord1 is stronger than ord2, then ord1 orders every % pair of elements that ord2 orders
stronger_eq?(ord1, ord2): MACRO bool = subset?(ord2, ord1)
stronger_eq?(ord2)(ord1): MACRO bool = subset?(ord2, ord1)
stronger?(ord1, ord2): MACRO bool = strict_subset?(ord2, ord1)
stronger?(ord2)(ord1): MACRO bool = strict_subset?(ord2, ord1)
% Weaker orders: if ord1 is weaker than ord2, then ord2 orders every % pair of elements that ord1 orders
weaker_eq?(ord1, ord2): MACRO bool = subset?(ord1, ord2)
weaker_eq?(ord2)(ord1): MACRO bool = subset?(ord1, ord2)
weaker?(ord1, ord2): MACRO bool = strict_subset?(ord1, ord2)
weaker?(ord2)(ord1): MACRO bool = strict_subset?(ord1, ord2)
% ========================================================================== % Properties preserved by stronger/weaker orders % ==========================================================================
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.
