products/sources/formale Sprachen/Coq/proofs/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: patch-7.lisp   Sprache: Lisp

Untersuchung PVS©
(skolemization
 (skolemize_exists 0
  (skolemize_exists-1 nil 3314540935
   ("" (skolem!)
    (("" (prop)
      (("1" (inst + "LAMBDA d: epsilon(LAMBDA r: p!1(d, r))")
        (("1" (skolem!)
          (("1" (inst?)
            (("1" (use "epsilon_ax[R]")
              (("1" (replace*) nil nil)
               ("2" (skolem!) (("2" (inst?) nil nil)) nil))
              nil))
            nil))
          nil)
         ("2" (skolem!)
          (("2" (inst - "d!1")
            (("2" (skolem!) (("2" (inst?) nil nil)) nil)) nil))
          nil))
        nil)
       ("2" (skosimp*) (("2" (inst?) (("2" (inst?) nil nil)) nil))
        nil))
      nil))
    nil)
   ((epsilon_ax formula-decl nil epsilons nil)
    (epsilon const-decl "T" epsilons nil)
    (pred type-eq-decl nil defined_types nil)
    (D formal-type-decl nil skolemization nil)
    (R formal-type-decl nil skolemization nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (TRUE const-decl "bool" booleans nil))
   shostak))
 (skolemize_forall 0
  (skolemize_forall-1 nil 3314541090
   ("" (skolem!)
    (("" (prop)
      (("1" (skosimp*) (("1" (inst?) (("1" (inst?) nil nil)) nil)) nil)
       ("2" (inst - "LAMBDA d: epsilon(LAMBDA r: NOT p!1(d, r))")
        (("1" (skolem!)
          (("1" (inst?)
            (("1" (use "epsilon_ax[R]")
              (("1" (prop)
                (("1" (hide -1)
                  (("1" (skolem!) (("1" (inst?) nil nil)) nil)) nil))
                nil)
               ("2" (hide -1)
                (("2" (skolem!) (("2" (inst?) nil nil)) nil)) nil))
              nil))
            nil))
          nil)
         ("2" (skolem!)
          (("2" (inst 2 "d!1")
            (("2" (skolem!) (("2" (inst?) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((D formal-type-decl nil skolemization nil)
    (R formal-type-decl nil skolemization nil)
    (epsilon_ax formula-decl nil epsilons nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (epsilon const-decl "T" epsilons nil)
    (pred type-eq-decl nil defined_types nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (TRUE const-decl "bool" booleans nil))
   shostak)))


¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.18Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤



Druckansicht
unsichere Verbindung
Druckansicht
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff