Quelle clock_shift.pvs Sprache: 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

quality89%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.