| products/Sources/formale Sprachen/Cobol/Test-Suite/SQL M/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: clock_minmax.pvs Sprache: Unknown
|
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 [ zur Elbe Produktseite wechseln0.11Quellennavigators Analyse erneut starten ] |