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 Thinking Intellekt

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/PVS/fault_tolerance/

Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Sprache: PVS

Untersuchung 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