products/sources/formale sprachen/PVS/pvs-emacs/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: extra.el   Sprache: Unknown

Spracherkennung für: .el vermutete Sprache: Scala {Scala[104] Lisp[107] Isabelle[136]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]

(defun complete-oracle-name (msg enabled)
  (let* ((oracles (pvs-send-and-wait  
     (format "(extra-list-oracle-names %s)" enabled)
     nil nil 'list))
  (oracle  (completing-read msg
       (mapcar 'list oracles) nil t)))
    (if (equal oracle "")
 (error "Must provide a oracle name")
      (list oracle))))

(defpvs disable-oracle prove (oracle)
  "Disable oracle.

Disable external oracle."
  (interactive (complete-oracle-name "Disable external oracle: " t))
  (confirm-not-in-checker)
  (pvs-bury-output)
  (save-some-pvs-buffers)
  (pvs-send-and-wait (format "(extra-disable-oracle '%s)" oracle)
       nil nil 'dont-care))

(defpvs enable-oracle prove (oracle)
  "Enable oracle.

Enable external oracle."
  (interactive (complete-oracle-name "Enable external oracle: " nil))
  (confirm-not-in-checker)
  (pvs-bury-output)
  (save-some-pvs-buffers)
  (pvs-send-and-wait (format "(extra-enable-oracle '%s)" oracle)
       nil nil 'dont-care))

[ Dauer der Verarbeitung: 0.54 Sekunden  ]