Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/PVS/structures/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 7.10.2014 mit Größe 1 kB

Quelle Unit_adt.pvs Sprache: PVS

%%% ADT file generated from Unit

Unit_adt: THEORY
BEGIN

  Unit: TYPE

  unit?: [Unit -> boolean]

  unit: (unit?)

  Unit_ord: [Unit -> upto(0)]

  Unit_ord_defaxiom: AXIOM Unit_ord(unit) = 0;

  ord(x: Unit): [Unit -> upto(0)] = CASES x OF unit: 0 ENDCASES

  Unit_inclusive: AXIOM FORALL (Unit_var: Unit): unit?(Unit_var);

  Unit_induction: AXIOM
    FORALL (p: [Unit -> boolean]):
      p(unit) IMPLIES (FORALL (Unit_var: Unit): p(Unit_var));

  subterm(x: Unit, y: Unit):  boolean = x = y;

  <<:  (strict_well_founded?[Unit]) = LAMBDA (x, y: Unit): FALSE;

  Unit_well_founded: AXIOM strict_well_founded?[Unit](<<);
END Unit_adt

Unit_adt_reduce[range: TYPE]: THEORY
BEGIN

  IMPORTING Unit_adt

  reduce(unit?_fun: range):  [Unit -> range] =
      LAMBDA (Unit_adtvar: Unit):
        LET red: [Unit -> range] = reduce(unit?_fun) IN
          CASES Unit_adtvar OF unit: unit?_fun ENDCASES;

  REDUCE(unit?_fun: [Unit -> range]):  [Unit -> range] =
      LAMBDA (Unit_adtvar: Unit):
        LET red: [Unit -> range] = REDUCE(unit?_fun) IN
          CASES Unit_adtvar OF unit: unit?_fun(Unit_adtvar) ENDCASES;
END Unit_adt_reduce

quality65%

¤ 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.