Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: protocol.pvs Sprache: PVS

Original von: 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

¤ 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.