products/sources/formale Sprachen/PVS/orders image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: lattices.pvs   Sprache: PVS

Original von: PVS©

% Author: Alfons Geser ([email protected]), National Institute of Aerospace
% Date: Oct 2004
%
% add_preserves_tightly_bounded and union_preserves_tightly_bounded added
% 13 Jan 2005 by Jerry James ([email protected])

lattices[
  T: TYPE,
  (IMPORTING bounded_orders[T])
  <=: (lattice?[T])
]: THEORY

BEGIN

  IMPORTING
    lower_semilattices[T, <=],
    upper_semilattices[T, <=]

  t: VAR T
  tb, tb2: VAR (tightly_bounded?(<=))

  finite_set_is_tightly_bounded: JUDGEMENT
    non_empty_finite_set[T] SUBTYPE_OF (tightly_bounded?(<=))

  add_preserves_tightly_bounded: JUDGEMENT
    add(t, tb) HAS_TYPE (tightly_bounded?(<=))

  union_preserves_tightly_bounded: JUDGEMENT
    union(tb, tb2) HAS_TYPE (tightly_bounded?(<=))

END lattices

¤ Dauer der Verarbeitung: 0.2 Sekunden  (vorverarbeitet)  ¤





Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




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.


Bot Zugriff