Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: patch-104.lisp Sprache: Lisp

Original von: PVS^©

;;
;; proveit-init.lisp
;; Release: ProofLite-6.0.9 (3/14/14)
;;
;; Contact: Cesar Munoz ([email protected])
;; NASA Langley Research Center
;; http://shemesh.larc.nasa.gov/people/cam/ProofLite
;;
;; Copyright (c) 2011-2012 United States Government as represented by
;; the National Aeronautics and Space Administration.  No copyright
;; is claimed in the United States under Title 17, U.S.Code. All Other
;; Rights Reserved.
;;

(in-package :pvs)

(defun eq-thf (decl thf)
  (and (string= (format nil "~a" (id decl))
  (car thf))))

;; Split string given a character
(defun split (str char)
  (when str
    (let ((pos (position char str)))
      (if pos
   (let ((hd (subseq str 0 pos))
  (tl (subseq str (+ pos 1))))
     (cons hd (split tl char)))
(list str)))))

;; Converts a string "th.f1:..:fn into a list ("th" "f1" ... "fn"),
(defun thf2list (thf)
  (let* ((l (split thf #\.)))
    (cons (car l) (split (cadr l) #\:))))

;; l is a sorted list of the form (("th" "f1" .. "fm") ...),
;; thf is an element of the form ("thg" "g1" .. "gk")
(defun thmerge (l thf)
  (cond ((and l thf)
  (if (string= (caar l) (car thf))
      (thmerge (cdr l) (append thf (cdar l)))
    (cons thf (thmerge (cdr l) (car l)))))
(l
  (thmerge (cdr l) (car l)))
(thf
  (list thf))))

;; Converts a list ("th.f1:..fn" ...) into a list (... ("th" "f1" .. "fm") ...)
;; that is alpabethically ordered and where formulas of the same theory are
;; put together (theories without formulas are removed)
(defun thfs2list (thsf)
  (let* ((l (sort (remove-if-not
     #'cdr
     (mapcar #'thf2list thsf))
    #'string<= :key #'car)))
    (thmerge l nil)))

(defun proveit-status-proof-theories (theories thfs)
  (if theories
      (let ((*disable-gc-printout* t))
(pvs-buffer "PVS Status"
   (with-output-to-string
       (*standard-output*)
     (proveit-proof-summaries theories thfs))
   t))
      (pvs-message "No theories given")))

(defun proveit-proof-summaries (theory-ids thfs
    &optional filename)
  (let ((tot 0) (proved 0) (unfin 0) (untried 0) (time 0))
    (when filename
      (format t "~2%Proof summary for file ~a.pvs" filename))
    (dolist (theory theory-ids)
         (let ((thf (car (member theory thfs :test #'eq-thf))))
    (multiple-value-bind (to pr uf ut tm)
        (proveit-proof-summary theory thf (when filename 2))
      (incf tot to) (incf proved pr) (incf unfin uf) (incf untried ut)
      (incf time tm))))
    (if filename
(format t "~2% Totals for ~a.pvs: " filename)
(format t "~2%Grand Totals: "))
    (format t "~d proofs, ~d attempted, ~d succeeded (~,2f s)"
      tot (+ proved unfin) proved time)
    (values tot proved unfin untried time)))

(defun proveit-proof-summary (theory-id thf &optional (indent 0))
  (if (null thf)
      (format t "~2%~vTProof summary for theory ~a" indent (ref-to-id theory-id))
    (format t "~2%~vTProof summary for formulas ~a in theory ~a" indent
     (cdr thf) (ref-to-id theory-id)))
  (let* ((tot 0) (proved 0) (unfin 0) (untried 0) (time 0)
  (theory (get-theory theory-id))
  (valid? (or (and theory
     (from-prelude? theory))
       (valid-proofs-file (context-entry-of theory-id)))))
    (if (and theory
      (typechecked? theory))
(let* ((fdecls (provable-formulas theory))
        (maxtime (/ (reduce #'max fdecls
       :key #'(lambda (d)
         (or (run-proof-time d) 0))
       :initial-value 0)
      internal-time-units-per-second))
        (statuslength 20) ; "proved - incomplete "
        (dplength (+ (apply #'max
         (mapcar #'(lambda (x) (length (string x)))
    *decision-procedures*))
       2))
        (timelength (length (format nil "~,2f" maxtime)))
        (idlength (- 79 4 statuslength dplength timelength 4 3)))
   (dolist (decl fdecls)
     (let ((dof (member (format nil "~a" (id decl)) (cdr thf)
          :test #'string=)))
        (when (or (null thf) dof)
   (let ((tm (if (run-proof-time decl)
          (/ (run-proof-time decl)
      internal-time-units-per-second 1.0)
        0)))
     (incf tot)
     (cond ((proved? decl)
     (incf proved))
    ((justification decl) (incf unfin))
    (t (incf untried)))
     (incf time tm)
     (format t "~% ~v,1,0,'.a...~19a [~a](~a s)"
       idlength
       (id decl)
       (proof-status-string decl)
       (if (justification decl)
    (decision-procedure-used decl)
    "Untried")
       (if (run-proof-time decl)
    (format nil "~v,2f" timelength tm)
    (format nil "~v" timelength))))))))
(let ((te (get-context-theory-entry theory-id)))
   (mapc #'(lambda (fe)
      (let ((status (fe-status fe)))
        (format t "~% ~52,1,0,'.a...~(~10a~)"
   (fe-id fe)
   (fe-proof-status-string fe valid?))
        (incf tot)
        (case status
   ((proved-complete proved-incomplete)
    (if valid?
        (incf proved)
        (incf unfin)))
   ((unchecked unfinished)
    (incf unfin))
   (t (incf untried)))))
  (te-formula-info te))))
    (format t "~% Theory totals: ~d formulas, ~d attempted, ~d succeeded ~
               (~,2f s)"
      tot (+ proved unfin) proved
      (/ (reduce #'+ (provable-formulas theory)
   :key #'(lambda (d) (or (run-proof-time d) 0))
   :initial-value 0)
  internal-time-units-per-second))
    (values tot proved unfin untried time)))

(defun proveit-theories (theories retry? thfs traces
      &optional txtproofs texproofs use-default-dp?)
  (let ((*use-default-dp?* use-default-dp?))
    (when texproofs
      (with-open-file
       (texfile
(ensure-directories-exist
  (pathname "pvstex/README.txt"))
:direction :output
:if-does-not-exist :create
:if-exists :supersede)
       (format texfile "To generate PDF files type: pdflatex main-.tex~%")))
    (read-strategies-files)
    (dolist (theory theories)
      (let ((thf (car (member theory thfs :test #'eq-thf))))
(if (null thf)
     (pvs-message "Proving theory ~a" (id theory))
   (pvs-message "Proving formulas ~a in theory ~a"
         (cdr thf) (id theory)))
(let ((*justifications-changed?* nil))
   (dolist (decl (provable-formulas theory))
     (let ((dof (member (format nil "~a" (id decl)) (cdr thf)
          :test #'string=)))
       (when (or (null thf) dof)
  (setq *last-proof* (pvs-prove-decl decl retry?))
  (when txtproofs
    (with-open-file
     (*standard-output*
      (ensure-directories-exist
       (pathname (format nil "pvstxt/~a.txt" (id decl))))
      :direction :output
      :if-does-not-exist :create
      :if-exists :supersede)
     (report-proof *last-proof*)))
  (when texproofs
    (latex-proof (format nil "~a.tex" (id decl)) t)
    (rename-file (format nil "~a.tex" (id decl))
          (format nil "pvstex/~a.tex" (id decl)))
    (rename-file "pvs-files.tex"
          (format nil "pvstex/main-~a.tex" (id decl)))))))
   (when *justifications-changed?*
     (save-all-proofs *current-theory*)))))))

(defun now-today ()
  (multiple-value-bind (s mi h d mo y dow dst tz)
         (get-decoded-time)
         (declare (ignore tz dst dow))
         (format nil "~a:~a:~a ~a/~a/~a" h mi s mo d y)))

(defun proveit ()
  (let* ((proveitversion (environment-variable "PROVEITVERSION"))
  (context (environment-variable "PROVEITPVSCONTEXT"))
  (pvsfile (environment-variable "PROVEITPVSFILE"))
  (baseout (environment-variable "PROVEITBASEOUT"))
  (import (read-from-string
    (environment-variable "PROVEITLISPIMPORT")))
  (scripts (read-from-string
     (environment-variable "PROVEITLISPSCRIPTS")))
  (traces (read-from-string
    (environment-variable "PROVEITLISPTRACES")))
  (force (read-from-string
   (environment-variable "PROVEITLISPFORCE")))
  (typecheckonly (read-from-string
    (environment-variable "PROVEITLISPTYPECHECK")))
  (txtproofs (read-from-string
       (environment-variable "PROVEITLISPTXTPROOFS")))
  (texproofs (read-from-string
       (environment-variable "PROVEITLISPTEXPROOFS")))
  (preludext (remove-duplicates
       (read-from-string
        (environment-variable "PROVEITLISPPRELUDEXT"))
       :test #'string=))
  (disable (remove-duplicates
     (read-from-string
      (environment-variable "PROVEITLISPDISABLE"))
     :test #'string=))
  (enable (remove-duplicates
    (read-from-string
     (environment-variable "PROVEITLISPENABLE"))
    :test #'string=))
  (thfs (thfs2list (read-from-string
      (environment-variable "PROVEITLISPTHFS"))))
  (theories (remove-duplicates
         (read-from-string
   (environment-variable "PROVEITLISPTHEORIES"))
       :test #'string=))
  (dependencies (environment-variable "PROVEITLISPDEPENDENCIES"))
  (*print-readably* nil)
  (*noninteractive* t)
  (*pvs-verbose* (if traces 3 2)))
    (when (and pvsfile (string/= pvsfile ""))
      (multiple-value-bind
   (val err)
   (handler-case
    (ignore-errors
      (format t "~%*** ~%*** ~a (~a)~%*** Generated by ~a~%"
       pvsfile (now-today) proveitversion)
      (extra-disable-but disable enable)
      (let ((orcls (extra-list-oracles)))
        (when orcls
   (format  t "*** Trusted Oracles~%")
   (loop for orcl in orcls
         do (format t "*** ~a: ~a~%"
      (car orcl) (cdr orcl)))))
      (format t "*** ")
      (change-context (probe-file context))
      (dolist (prelude preludext) (load-prelude-library prelude t))
      (typecheck-file pvsfile nil nil nil t)
      (save-context)
      (let* ((theory-names (or theories (theories-in-file pvsfile)))
      (pvstheories
       (if import (imported-theories-in-theories theory-names)
         (mapcar #'get-typechecked-theory theory-names)))
      (depfile (pathname (format nil "pvsbin/~a.dep" baseout))))
        (when (equal dependencies "t")
   (with-open-file
    (stream (ensure-directories-exist depfile)
     :direction :output
     :if-exists :supersede
     :if-does-not-exist :create)
    (format stream "/~{~a~^,~}~%" (mapcar #'id pvstheories))
    (maphash
     #'(lambda (k e)
         (format stream "~a~{~a~^,~}~%" k
          (loop for th being the hash-keys in (car e) collect th)))
     *imported-libraries*)
    (loop for th in pvstheories
   for idth = (id th)
   do (format stream "~a:~{~a~^,~}~%" idth
       (mapcar
        #'(lambda(x)
     (if (typep x '(or library-theory
         library-datatype
         library-codatatype))
         (format nil "~a@~a"
          (string-right-trim
           "/" (lib-ref x))
          (id x))
       (id x)))
        (immediate-theories-in-theory idth))))))
        (if typecheckonly
     (format t "~%File ~a.pvs typechecked" pvsfile)
   (let ((pvstheories
   (remove-if #'(lambda (th) (typep th '(or datatype codatatype)))
       pvstheories)))
     (when scripts
       (dolist (theory pvstheories)
         (install-prooflite-scripts (filename theory) (id theory) 0
        force)))
     (proveit-theories pvstheories force thfs traces txtproofs texproofs)
     (proveit-status-proof-theories pvstheories thfs))))
      (save-context)
      t)
    (storage-condition
     (condition)
     (values nil condition)))
(when err
   (format t "~%~a (~a)~%" err pvsfile)
   (bye 0))))
    (fresh-line)
    (bye 1)))

¤ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.