Quelle inexact_reduce.pvs Sprache: PVS

%
%
% Purpose : validity and agreement properties for a multi-stage inexact
%           exchange with the results-based fault model.
%
%

inexact_reduce
[
    N   : [nat -> posnat],
    error: [nat -> real]
] : THEORY

  BEGIN

  IMPORTING
    inexact_comm[N],
    protocol[N, real],
    k_ordered[N, real, <=, error],
    inexact_reduce_stage,
    reals@sigma_nat

  i, j, k: VAR nat
  v: VAR real

  sent:  VAR sent_vec
  rcvd:  VAR rcvd_matrix
  check: VAR check_function

  epsilon, eps_u, eps_l, eps: VAR [nat -> nonneg_real]
  delta : VAR nonneg_real

  node_set: VAR [i: nat -> non_empty_finite_set[below(N(i))]]

  tau: VAR [j: nat -> tau_type]
  idx: VAR [nat -> nat]
  cf: VAR k_consensus_function

% Main results
  lower_validity: THEOREM
      protocol(reduce_choice(tau, cf), sent, rcvd, check, j, j + k) AND
      quorum_lower?(sent, rcvd, check, tau, eps_l, j, j + k) AND
      enabled_within?(rcvd, check, j, j + k)(node_set)
    IMPLIES
      v_min(sent, node_set)(j) - sigma(j, j + k - 1, eps_l) <= v_min(sent, node_set)(j + k)

  upper_validity: THEOREM
      protocol(reduce_choice(tau, cf), sent, rcvd, check, j, j + k) AND
      quorum_upper?(sent, rcvd, check, tau, eps_u, j, j + k) AND
      enabled_within?(rcvd, check, j, j + k)(node_set)
    IMPLIES
      v_max(sent, node_set)(j + k) <= v_max(sent, node_set)(j) + sigma(j, j + k - 1, eps_u)

  agreement_propagation: THEOREM
      protocol(reduce_choice(tau, cf), sent, rcvd, check, j, j + k) AND
      quorum_imprecision?(sent, rcvd, check, tau, epsilon, j, j + k) AND
      enabled_within?(rcvd, check, j, j + k)(node_set) AND
      v_max(sent, node_set)(j) - v_min(sent, node_set)(j) <= delta
    IMPLIES
      v_max(sent, node_set)(j + k) - v_min(sent, node_set)(j + k)
        <= delta + sigma(j, j + k - 1, epsilon)

  X: VAR posnat

  convergent_stage?(rcvd, check, tau, epsilon, cf, X, j, k): bool =
    EXISTS i: j <= i AND i < k AND
      overlap_imprecision?[N(i), N(i + 1), error(i)](rcvd(i), check(i), tau(i), epsilon(i)) AND
      convergent?(cf(i), max_length[N(i), N(i + 1), real, <=, error(i)](rcvd(i), check(i), tau(i)), X)

  convergence: THEOREM
      protocol(reduce_choice(tau, cf), sent, rcvd, check, j, j + k) AND
      quorum_imprecision?(sent, rcvd, check, tau, epsilon, j, j + k) AND
      enabled_within?(rcvd, check, j, j + k)(node_set) AND
      convergent_stage?(rcvd, check, tau, epsilon, cf, X, j, j + k) AND
      v_max(sent, node_set)(j) - v_min(sent, node_set)(j) <= delta
    IMPLIES
      v_max(sent, node_set)(j + k) - v_min(sent, node_set)(j + k)
        <= delta * ((X - 1) / X) + sigma(j, j + k - 1, epsilon)

  agreement_generation: THEOREM
      protocol(reduce_choice(tau, cf), sent, rcvd, check, j, j + k) AND
      exists_all_symmetric?(sent, rcvd, check, tau, epsilon, cf, j, j + k) AND
      enabled_within?(rcvd, check, j, j + k)(node_set)
    IMPLIES
      v_max(sent, node_set)(j + k) - v_min(sent, node_set)(j + k) <= sigma(j, j + k - 1, epsilon)

END inexact_reduce

quality97%

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