Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: clock_shift.pvs Sprache: PVS

Original von: PVS^©

%
%
% Purpose : Results to derive relationships between clocks,
%           especially to show that two clocks share the same oscillator.
%
%

clock_shift[ rho:nonneg_real, N: posnat]: THEORY

  BEGIN

  IMPORTING inverse_clocks[rho]

  c, c1, c2: VAR [below(N) -> good_clock]
  T, T1, T2: VAR integer
  X: VAR nat

  n, n1, n2: VAR below(N)

  local_event, le1, le2: VAR [below(N) -> real]

  all_clock_edge?(c, local_event): bool = FORALL n: clock_edge?(c(n), local_event(n))

  offset(c, T)(local_event)(n): real = offset(c(n), T)(local_event(n))

  same_edges?(c1, c2): bool = FORALL n: offset_clocks?(c1(n), c2(n))

  offset_left_edge: LEMMA
      clock_edge?(c(n), local_event(n)) AND
      0 <= T
    IMPLIES
      T / rate <= offset(c, T)(local_event)(n) - local_event(n)

  offset_left: LEMMA
      X / rate < offset(c, X)(local_event)(n) - local_event(n) + rate

  offset_right_edge: LEMMA
      clock_edge?(c(n), local_event(n)) AND
      0 <= T
    IMPLIES
      offset(c, T)(local_event)(n) - local_event(n) <= rate * T

  offset_right: LEMMA
       offset(c, X)(local_event)(n) - local_event(n) <= rate * X

  offset_zero: LEMMA
      all_clock_edge?(c, local_event)
    IMPLIES
      offset(c, 0)(local_event) = local_event

  offset_drift: LEMMA
      offset(c, X)(local_event)(n2) - offset(c, X)(local_event)(n1)
        < local_event(n2) - local_event(n1) + drift * X + rate

  offset_nondecreasing: LEMMA
    le1(n) <= le2(n) IMPLIES offset(c, T)(le1)(n) <= offset(c, T)(le2)(n)

  offset_drift_edge: LEMMA
      clock_edge?(c(n1), le1(n1)) AND
      clock_edge?(c(n2), le2(n2))
    IMPLIES
      offset(c, X)(le2)(n2) - offset(c, X)(le1)(n1)
        <= le2(n2) - le1(n1) + drift * X

  double_offset: LEMMA
    offset(c, T1)(offset(c, T2)(local_event)) = offset(c, T1 + T2)(local_event)

  offset_same: LEMMA
      same_edges?(c1, c2)
    IMPLIES
      (offset(c1, T1 + T2)(le1) = offset(c2, T1 + T2)(le2) IFF offset(c1, T2)(le1) = offset(c2, T2)(le2))

  offset_same2: LEMMA
      same_edges?(c1, c2) AND
      all_clock_edge?(c1, le1) AND
      all_clock_edge?(c2, le2)
    IMPLIES
      (offset(c1, T1)(le1) = offset(c2, T1)(le2) IFF le1 = le2)

  END clock_shift

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