Quelle majority_properties.pvs Sprache: PVS

%
%
% Purpose : core "majority" results, including a majority choice
%           function, validity and agreement properties
%
%

majority_properties[N: posnat, T:TYPE+]: THEORY

BEGIN

  IMPORTING
    finite_seqs[T],
    finite_sets@finite_sets_card_eq,
    pigeonhole[below(N)],
    node[N, T]

  v, v1, v2: VAR vec
  e, node_set: VAR nodeid_set
  d, t: VAR T

  mf: VAR majority_function

  majority(mf)(v, e): T = mf(vec2seq(v, e))

  majority_exists?(v, e): bool = maj_exists(vec2seq(v, e))

  majority_value_set(e, v)(t) : bool =
    2 * card(uniform_nodes(e, v, t)) > card(e)

  is_majority: LEMMA  majority_value_set(e, v)(t) IFF is_majority(t, vec2seq(v, e))

  majority_value_subset: LEMMA
      majority_value_set(e, v)(t)
    IFF
      majority_subset?(uniform_nodes(e, v, t), e)

  uniform_majority: LEMMA
      majority_subset?(node_set, e) AND
      uniform?(v, t)(node_set)
    IMPLIES
      majority_value_set(e, v)(t)

  majority_validity: LEMMA
      majority_value_set(e, v)(t)
    IMPLIES
      majority(mf)(v, e) = t

  agreement_generation: THEOREM
      enabled_symmetric?(e, v1, v2)
    IMPLIES
      majority(mf)(v1, e) = majority(mf)(v2, e)

END majority_properties

quality100%

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