Quelle protocol.pvs Sprache: PVS

%
%
% Purpose : Build the messages that a destination sends, given
%           the messages it receives.
%
%

protocol
[
    N   : [nat -> posnat],  % Number of source nodes at each stage
    T   : TYPE+
]: THEORY

BEGIN

  i, j, k: VAR nat

  IMPORTING node_functions[N, T]

  sent:   VAR sent_vec
  rcvd:   VAR rcvd_matrix

  check:  VAR check_function
  choice: VAR choice_function
  compute:VAR compute_function

  %
  % Models of protocol for stages j..k
  %

  % no computation after the choice
  protocol(choice, sent, rcvd, check, j, k) : bool =
    FORALL i : j <= i AND i < k IMPLIES
      sent(i + 1) = choice(i)(rcvd(i), check(i))

  % arbitrary compute function after choice.  The function can
  % be different in each stage and different for each node
  % in the stage.  This means that the function can be based
  % on information that is local only to the node.
  protocol(compute, choice, sent, rcvd, check, j, k) : bool =
    FORALL i : j <= i AND i < k IMPLIES
      sent(i + 1) = compute(i+1)(choice(i)(rcvd(i), check(i)))

%  identity: compute_function = LAMBDA j: id[vec[N(j), T]]

%  identity_compute_same: LEMMA
%    protocol(identity, choice, sent, rcvd, check, j, k)
%      IFF protocol(choice, sent, rcvd, check, j, k)

  %
  % Models of protocol for stages 0..k
  %

  % no computation after the choice
  protocol(sent, rcvd, check, choice, k) : bool =
    FORALL i : i < k IMPLIES
      sent(i + 1) = choice(i)(rcvd(i), check(i))

  % arbitrary compute function after choice.  The function can
  % be different in each stage and different for each node
  % in the stage.  This means that the function can be based
  % on information that is local only to the node.
%  protocol(sent, rcvd, check, choice, compute, k) : bool =
%    FORALL i : i < k IMPLIES
%      sent(i + 1) = compute(i+1)(choice(i)(rcvd(i), check(i)))

  % correspondence results
  protocol_rw: LEMMA
    protocol(sent, rcvd, check, choice, k)
      = protocol(choice, sent, rcvd, check, 0, k)

%  protocol_compute_rw: LEMMA
%    protocol(sent, rcvd, check, choice, compute, k)
%      = protocol(compute, choice, sent, rcvd, check, 0, k)

END protocol

quality70%

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