products/sources/formale sprachen/Isabelle/Tools/Spec_Check/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: comm_integration.prf   Sprache: Unknown

(comm_integration
 (quorum_correct_integration 0
  (quorum_correct_integration-1 nil 3399298560
   ("" (skosimp*)
    (("" (expand "quorum_correct?")
      (("" (skosimp*)
        (("" (inst?)
          (("" (assert)
            (("" (expand "rcvd")
              ((""
                (use "quorum_correct_integration[N(i!1), N(1 + i!1), T]")
                (("" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((quorum_correct? const-decl "bool" exact_comm nil)
    (quorum_correct? const-decl "bool" comm_integration nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (rcvd const-decl "[below(N(i + 1)) -> [below(N(i)) -> UT]]"
     comm_integration nil)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (message type-decl nil message_adt nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (garbled? adt-recognizer-decl "[message -> boolean]" message_adt
     nil)
    (garbled adt-constructor-decl "(garbled?)" message_adt nil)
    (msg_checker nonempty-type-eq-decl nil comm_integration_stage nil)
    (valid_check_stage type-eq-decl nil comm_integration_stage nil)
    (valid_check_function type-eq-decl nil comm_integration nil)
    (sent_vec_stage type-eq-decl nil node_functions_stage nil)
    (UT type-eq-decl nil comm_integration nil)
    (fault_class type-decl nil integration_fault_model nil)
    (node_status type-eq-decl nil integration_fault_model nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (tau_type type-eq-decl nil tau_declaration nil)
    (T formal-nonempty-type-decl nil comm_integration nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (N formal-const-decl "[nat -> posnat]" comm_integration nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (quorum_correct_integration formula-decl nil comm_integration_stage
     nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (majority_correct_rw 0
  (majority_correct_rw-1 nil 3399298055
   ("" (skosimp*)
    (("" (expand "majority_correct?")
      (("" (expand "quorum_correct?")
        (("" (prop)
          (("1" (skosimp*)
            (("1" (inst?)
              (("1" (assert)
                (("1" (rewrite "majority_correct_rw")
                  (("1" (expand "mid" 1) (("1" (propax) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (skosimp*)
            (("2" (inst?)
              (("2" (assert)
                (("2" (rewrite "majority_correct_rw")
                  (("2" (expand "mid" -1) (("2" (propax) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((majority_correct? const-decl "bool" comm_integration nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (majority_correct_rw formula-decl nil comm_integration_stage nil)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (message type-decl nil message_adt nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (garbled? adt-recognizer-decl "[message -> boolean]" message_adt
     nil)
    (garbled adt-constructor-decl "(garbled?)" message_adt nil)
    (msg_checker nonempty-type-eq-decl nil comm_integration_stage nil)
    (valid_check_stage type-eq-decl nil comm_integration_stage nil)
    (valid_check_function type-eq-decl nil comm_integration nil)
    (sent_vec_stage type-eq-decl nil node_functions_stage nil)
    (UT type-eq-decl nil comm_integration nil)
    (fault_class type-decl nil integration_fault_model nil)
    (node_status type-eq-decl nil integration_fault_model nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (N formal-const-decl "[nat -> posnat]" comm_integration nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (T formal-nonempty-type-decl nil comm_integration nil)
    (mid const-decl "tau_type" exact_comm nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (quorum_correct? const-decl "bool" comm_integration nil))
   shostak))
 (all_symmetric_integration 0
  (all_symmetric_integration-1 nil 3399299095
   ("" (skosimp*)
    (("" (expand "exists_all_symmetric?")
      (("" (skosimp*)
        (("" (inst?)
          (("" (assert)
            (("" (use "quorum_correct_integration")
              (("" (assert)
                ((""
                  (use "all_symmetric_integration[N(i!1), N(1 + i!1), T]")
                  (("" (assert)
                    (("" (expand "rcvd" +) (("" (propax) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((exists_all_symmetric? const-decl "bool" exact_comm nil)
    (exists_all_symmetric? const-decl "bool" comm_integration nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (quorum_correct_integration formula-decl nil comm_integration nil)
    (tau_type type-eq-decl nil tau_declaration nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (node_status type-eq-decl nil integration_fault_model nil)
    (fault_class type-decl nil integration_fault_model nil)
    (UT type-eq-decl nil comm_integration nil)
    (valid_check_function type-eq-decl nil comm_integration nil)
    (valid_check_stage type-eq-decl nil comm_integration_stage nil)
    (msg_checker nonempty-type-eq-decl nil comm_integration_stage nil)
    (garbled adt-constructor-decl "(garbled?)" message_adt nil)
    (garbled? adt-recognizer-decl "[message -> boolean]" message_adt
     nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (message type-decl nil message_adt nil)
    (T formal-nonempty-type-decl nil comm_integration nil)
    (below type-eq-decl nil naturalnumbers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (N formal-const-decl "[nat -> posnat]" comm_integration nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (< const-decl "bool" reals nil)
    (all_symmetric_integration formula-decl nil comm_integration_stage
     nil)
    (sent_vec_stage type-eq-decl nil node_functions_stage nil)
    (rcvd const-decl "[below(N(i + 1)) -> [below(N(i)) -> UT]]"
     comm_integration nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil))
   nil)))

[ Verzeichnis aufwärts0.6unsichere Verbindung  Übersetzung europäischer Sprachen durch Browser  ]