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/fault_tolerance/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 1 kB

Quelle clock_minmax.pvs Sprache: PVS

clock_minmax[rho : nonneg_real]: THEORY

  BEGIN

  IMPORTING
    physical_clocks[rho],
    finite_sets@finite_sets_minmax_props[real, <=],
    function_image_nonempty[good_clock, real]

  c: VAR good_clock
  T: VAR int

  participant: VAR non_empty_finite_set[good_clock]

  t_at(T)(c): real = c(T)

  clock_min(participant)(T): real = min(image(t_at(T), participant))
  clock_max(participant)(T): real = max(image(t_at(T), participant))

  clock_min_witness: LEMMA
    EXISTS c: participant(c) AND clock_min(participant)(T) = c(T)

  clock_max_witness: LEMMA
    EXISTS c: participant(c) AND clock_max(participant)(T) = c(T)

  clock_min_is_min: LEMMA
    participant(c) IMPLIES clock_min(participant)(T) <= c(T)

  clock_max_is_max: LEMMA
    participant(c) IMPLIES c(T) <= clock_max(participant)(T)

  clock_min_clock: JUDGEMENT clock_min(participant) HAS_TYPE good_clock
  clock_max_clock: JUDGEMENT clock_max(participant) HAS_TYPE good_clock

  hst: VAR [nat -> non_empty_finite_set[good_clock]]
  j: VAR nat

  ic_min(hst)(j): good_clock = clock_min(hst(j))
  ic_max(hst)(j): good_clock = clock_max(hst(j))

  END clock_minmax

quality81%

¤ Dauer der Verarbeitung: 0.10 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.