Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: timing_window.prf Sprache: PVS

Original von: PVS^©

%
%
% Purpose : properties of the min/max of the results
%           from a set of parallel nodes
%
%

select_minmax[N: posnat, T: TYPE+, <=: (total_order?[T])]: THEORY

  BEGIN

  IMPORTING
    finite_sets@finite_sets_minmax[T, <=],
    node[N, T],
    relations_extra[T]

  node_set: VAR non_empty_finite_set[below(N)]
  v: VAR vec
  n: VAR below(N)
  t: VAR T

  v_min(v, node_set): T = min(image(v, node_set))

  v_max(v, node_set): T = max(image(v, node_set))

  v_min_witness: LEMMA
    EXISTS n: node_set(n) AND v_min(v, node_set) = v(n)

  v_max_witness: LEMMA
    EXISTS n: node_set(n) AND v_max(v, node_set) = v(n)

  v_min_is_min: LEMMA
    node_set(n) IMPLIES v_min(v, node_set) <= v(n)

  v_max_is_max: LEMMA
    node_set(n) IMPLIES v(n) <= v_max(v, node_set)

  min_le_max: LEMMA
    v_min(v, node_set) <= v_max(v, node_set)

  min_le_max_alt: LEMMA
    v_max(v, node_set) = v_min(v, node_set) IFF
      (v_max(v, node_set) <= v_min(v, node_set))

  v_minmax_choose: LEMMA
    uniform?(v, t)(node_set) IFF
      (v_max(v, node_set) = v_min(v, node_set) AND v_min(v, node_set) = t)

  v_minmax_choose_alt: LEMMA
    uniform?(v, t)(node_set) IFF
      (v_max(v, node_set) <= t AND t <= v_min(v, node_set))

  END select_minmax

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