Quelle patch-103.lisp Sprache: Lisp

;;
;; prooflite.lisp
;; Release: ProofLite-6.0.9 (3/14/14)
;;
;; Contact: Cesar Munoz (cesar.a.munoz@nasa.gov)
;; 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.
;;

(defun associate-proof-with-formulas (theory-name formula-name strategy force)
  (let ((theory (get-typechecked-theory theory-name)))
    (if theory
(let* ((fname  (match-formula-name formula-name))
        (name   (car fname))
        (args   (cdr fname)))
   (if fname
       (let* ((regexp (expand-rex name))
       (str    (if force "" "untried "))
       (fdecls (remove-if-not
         #'(lambda (d)
      (and (formula-decl? d)
           (let ((idstr (format nil "~a" (id d))))
      (and (or (not (proofs d)) force)
           (pregexp-match regexp idstr)))))
         (all-decls theory))))
  (if fdecls
      (associate-proof-with-formula
       theory regexp (instantiate-script strategy args 1 "#")
       fdecls)
    (pvs-message
     "\"~a\" does not match any ~aformula" name str)))
     (pvs-message
      "\"~a\" is not a valid proof script header" formula-name)))
      (pvs-message "Theory ~a not found" theory-name))))

(defun associate-proof-with-formula (theory regexp strategy fdecls)
  (when fdecls
    (let* ((fdecl  (car fdecls))
           (match  (pregexp-match regexp (format nil "~a" (id fdecl))))
           (script (instantiate-script strategy match 0 "\\$")))
      (multiple-value-bind (strat err)
   #+(and allegro (not pvs6))
   (unwind-protect
       (progn (excl:set-case-mode :case-insensitive-lower)
       (ignore-errors (values (read-from-string script))))
     (excl:set-case-mode :case-sensitive-lower))
   #-(and allegro (not pvs6))
   (ignore-errors (values (read-from-string script)))
(let ((just (unless err
        (or (revert-justification strat)
     (revert-justification (list "" strat))
     strat))))
   (unless just
     (type-error script
       "Bad form for script~% ~s" script))
   (setf (justification fdecl) just)
   (save-all-proofs theory)
   (pvs-message "Proof script ~a was installed" (id fdecl)))))
    (associate-proof-with-formula theory regexp strategy (cdr fdecls))))

;; Returns a list of theory names defined in a PVS file
(defun theories-in-file (file)
   (mapcan #'(lambda (theofile)
        (and (or (string= (cadr theofile) file))
      (list (car theofile))))
    (cdr (collect-theories))))

;; Returns a list of theories imported in theory-names
(defun imported-theories-in-theories (theory-names)
  (remove-duplicates
   (mapcan #'(lambda (theo) (imported-theories-in-theory theo))
    theory-names)))

(defun my-collect-theory-usings (theory)
  (unless (or (memq theory *modules-visited*)
       (from-prelude? theory)
       (typep theory '(or library-datatype
     library-codatatype
     library-theory)))
    (let ((*current-theory* theory))
      (push theory *modules-visited*)
      (dolist (use (get-immediate-usings theory))
(let ((th (get-theory use)))
   (when th
     (my-collect-theory-usings
      (if (typep th 'rectype-theory)
   (get-typechecked-theory (generated-by th))
        th))))))))

;; Returns a list of immediately imported theories in the theory-name
(defun immediate-theories-in-theory (theory-name)
  (let ((theory (get-typechecked-theory theory-name)))
    (when theory
      (remove-duplicates
       (loop for use in (get-immediate-usings theory)
      for th = (get-theory use)
      when th
      unless (from-prelude? th)
      collect (if (typep th 'rectype-theory)
    (get-typechecked-theory (generated-by th))
         th))))))

;; Returns a list of theories imported in the theory-name
(defun imported-theories-in-theory (theory-name)
  (let ((theory (get-typechecked-theory theory-name)))
    (when theory
      (let* ((*modules-visited* nil))
(my-collect-theory-usings theory)
(nreverse *modules-visited*)))))

(defun trim-left (str)
  (string-left-trim '(#\Space #\Tab) str))

(defun trim-right (str)
  (string-right-trim '(#\Space #\Tab) str))

(defun trim (str)
  (string-trim '(#\Space #\Tab) str))

(defun ident () "([\\w\\*]+)")

(defun spaces () "[\\s\\t]*")

(defun greedyspaces () "(?)

(defun expand-rex (str)
  (format nil "^~a$" (pregexp-replace* "*" str "(.+)")))

(defun read-one-line (file)
  (let* ((str   (read-line file nil nil))
  (strim (when str (trim str))))
    (cond ((and (> (length strim) 3) (string= strim "%|-" :end1 3))
    strim)
   ((and (> (length strim) 0) (char= (elt strim 0) #\%))
    "%")
   (strim ""))))

(defun match-formula-name (str)
  (let ((match (cdr (pregexp-match
       (format nil "^~a(?:$|~a\\[(.*)\\]$)"
        (ident) (greedyspaces))
       str))))
    (when match
      (let* ((name (car match))
      (args (pregexp-split ";" (trim (cadr match))))
      (nargs (when (car args)
        (mapcar #'(lambda (x) (trim x)) args))))
(cons name nargs)))))

(defun is-proof-comment (str)
  (when (> (length str) 3) (trim-left (subseq str 3))))

(defun is-comment (str) (> (length str) 0))

(defun match-proof (str)
  (let ((match (pregexp-match-positions
  (format nil "^(.+):~a(?i:proof)\\b" (spaces))
  str)))
    (when match
      (cons (trim-right (subseq str (caadr match) (cdadr match)))
     (trim (subseq str (cdar match) (length str)))))))

(defun match-qed (str)
  (let ((match (pregexp-match "^(.*)\\b(?i:qed)$" str)))
    (when match
      (trim (cadr match)))))

(defun install-script (theory script formulas force)
  (when formulas
    (associate-proof-with-formulas theory (car formulas)
      (format nil "(\"\" ~a)" script) force)
    (install-script theory script (cdr formulas) force)))

(defun new-script (script new)
  (let ((notempty (> (length new) 0)))
    (cond ((and script notempty)
    (format nil "~a ~a" script new))
   (script script)
   (notempty new))))

(defun instantiate-script (script args n str)
  (if args
      (let ((new (pregexp-replace* (format nil "~a~a" str n) script
       (car args))))
(instantiate-script new (cdr args) (+ n 1) str))
    script))

(defun install-prooflite-scripts (filename theory line force)
  (with-open-file
   (file (format nil "~a.pvs" filename) :direction :input)
   (let* ((loc        (place (get-theory theory)))
   (lfrom      (aref loc 0))
   (lto        (aref loc 2)))
     (loop repeat (- lfrom 1) do (read-line file nil nil))
     (if (= line 0)
  (pvs-message "Installing proof scripts [Theory: ~a]"
        theory)
       (pvs-message "Installing proof script at line ~a [Theory: ~a]"
      line theory))
     (do ((str (read-one-line file))
   (n   lfrom)
   (formulas)
   (script))
  ((or (null str) (> n lto)))
  (let ((proofcomment (is-proof-comment str)))
    (cond (proofcomment
    (let* ((proof     (match-proof proofcomment))
    (formula   (car proof))
    (qed       (match-qed proofcomment)))
      (cond
       (formula
        (when (and script (< line n))
   (pvs-message
    "QED is missing in proof script(s) ~a [Theory: ~a]"
    formulas theory))
        (setq str (format nil "%|-~a" (cdr proof)))
        (setq formulas (cons formula
        (when (not script) formulas)))
        (setq script nil))
       (qed
        (let ((newscript (new-script script qed)))
   (when (and newscript formulas (<= line n))
     (install-script theory newscript
       (reverse formulas)
       force))
   (cond ((or (= line 0) (< n line))
          (setq str (read-one-line file))
          (setq n   (+ n 1))
          (setq formulas nil)
          (setq script nil))
         ((not formulas)
          (pvs-message
    "No script was installed [Theory: ~a]"
    theory)
          (setq str nil))
         (t (setq str nil)))))
       (t (setq str (read-one-line file))
   (setq n   (+ n 1))
   (setq script (new-script script proofcomment))))))
   ((is-comment str)
    (setq str (read-one-line file))
    (setq n   (+ n 1)))
   (t
    (when (and formulas (< line n))
      (pvs-message
       "QED is missing in proof script(s) ~a [Theory: ~a]"
       formulas theory))
    (cond ((or (= line 0) (< n line))
    (setq str (read-one-line file))
    (setq n   (+ n 1))
    (setq formulas nil)
    (setq script nil))
   ((and (< 0 line) (or (not formulas) (= line n)))
    (pvs-message "No script was installed [Theory: ~a]"
          theory)
    (setq str nil))
   (t (setq str nil))))))))))

(defun then-prooflite (script)
  (cond ((and
   (cdr script)
   (null (cddr script))
   (listp (caadr script)))
  (list (list 'spread
       (car script)
       (mapcar #'(lambda (s) (to-prooflite (cdr s)))
        (cadr script)))))
(script
  (cons (car script) (then-prooflite (cdr script))))))

(defun to-prooflite (script)
  (cond ((null (cdr script))
  (car script))
((and (null (cddr script))
       (listp (caadr script)))
  (car (then-prooflite script)))
(t
  (cons 'then (then-prooflite script)))))

(defun prooflite-script (fdecl)
  (when fdecl
    (if (justification fdecl)
(to-prooflite (cdr (editable-justification
        (justification fdecl))))
      (list 'postpone))))

(defun proof-to-prooflite-script (name line)
  (let* ((fdecl (formula-decl-to-prove name nil line "pvs")))
    (when fdecl
      (pvs-buffer
       "ProofLite"
       (with-output-to-string
  (out)
  (format out "~a : PROOF~%" (id fdecl))
  (write (prooflite-script fdecl)
  :stream out :pretty t :escape t
  :level nil :length nil
  :pprint-dispatch *proof-script-pprint-dispatch*)
  (format out "~%QED~%")))
      (list (aref (place fdecl) 2)))))

(defun find-formula (theory-name formula)
  (let ((theory (get-typechecked-theory theory-name)))
    (when theory
      (find-if #'(lambda (d) (and (formula-decl? d)
      (string= (format nil "~a" (id d))
        formula)))
        (all-decls theory)))))

(defun all-decl-names (theory-name)
  (let ((theory (get-typechecked-theory theory-name)))
    (when theory
      (mapcar #'(lambda (d) (format nil "~a" (id d)))
       (remove-if-not #'(lambda (d) (formula-decl? d))
        (all-decls theory))))))

(defun display-prooflite-script (theory formula)
  (let* ((fdecl (find-formula theory formula)))
    (when fdecl
      (pvs-buffer
       "ProofLite"
       (with-output-to-string
  (out)
  (format out "~a : PROOF~%" (id fdecl))
  (write (prooflite-script fdecl)
  :stream out :pretty t :escape t
  :level nil :length nil
  :pprint-dispatch *proof-script-pprint-dispatch*)
  (format out "~%QED~%"))))))

quality94%

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