Quelle order_strength.pvs Sprache: PVS

%-------------------------------------------------------------------------
%
%  "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
  % ==========================================================================

  stronger_reflexive: THEOREM
    FORALL ord1, ord2:
      stronger_eq?(ord1, ord2) AND reflexive?(ord2) => reflexive?(ord1)

  weaker_irreflexive: THEOREM
    FORALL ord1, ord2:
      weaker_eq?(ord1, ord2) AND irreflexive?(ord2) => irreflexive?(ord1)

  weaker_antisymmetric: THEOREM
    FORALL ord1, ord2:
      weaker_eq?(ord1, ord2) AND antisymmetric?(ord2) =>
       antisymmetric?(ord1)

END order_strength

quality89%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.