Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: clock_minmax.pvs Sprache: PVS

Original von: 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

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