Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 867

Synopsis:        Declaration generic function
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Wed Nov 17 14:15:00 2004
Originator:      Jerry James
Organization:    ittc.ku.edu
Release:         PVS 3.2

  I am running PVS 3.2 on a Fedora Core 2 system.  My .pvs.lisp contains
  the code given in response to bugs 861-863.  Using the PVS 3.2 libraries
  distributed by LaRC, the following theory provokes a PVS error.
  declaration_bug: THEORY
    IMPORTING sets_aux@well_ordered_finite[nat, <]
    below_set(S: set[nat])(n: (S)): finite_set[nat] =
        {m: nat | S(m) AND m < n}
   END declaration_bug
  Typecheck this theory, then attempt to prove below_set_TCC1.  Before the
  prompt appears, PVS triggers this error:
   Error: No methods applicable for generic function
         #<standard-generic-function declaration> with args
         (restrict[[real, real], [nat, nat], boolean](<)) of classes
    [condition type: program-error]
  Giving the restrict form instead of bare "<" in the IMPORTING clause
  does not help.  Changing the "<" in the definition of below_set to ">"
  also does not avoid the error.
  Jerry James
  Email: james@ittc.ku.edu -or- jamesj@acm.org
  WWW:   http://www.ittc.ku.edu/~james/


Moved the let for *bin-theories-set* before the call to
fetch-object-from-file in  get-theory-from-binfile to ensure any theories
added to *pvs-modules* are removed if there is an error.

(defun get-theory-from-binfile (filename)
  (let* ((file (make-binpath filename))
	 (start-time (get-internal-real-time))
	 (*bin-theories-set* nil)
	 (vtheory (ignore-lisp-errors (fetch-object-from-file file)))
	 (load-time (get-internal-real-time)))
    (if (and (listp vtheory)
	     (integerp (car vtheory))
	     (= (car vtheory) *binfile-version*))
	(let* ((theory (cdr vtheory))
	       (*restore-object-hash* (make-hash-table :test #'eq))
	       (*restore-objects-seen* nil)
	       (*assert-if-arith-hash* (make-hash-table :test #'eq))
	       (*subtype-of-hash* (make-hash-table :test #'equal))
	       (*current-context* (prerestore-context (saved-context theory))))
	  (assert (current-theory))
	  (assert (judgement-types-hash (judgements *current-context*)))
	  (restore-object theory)
	  (assert (datatype-or-module? theory))
	  (assert (not (eq (lhash-next (declarations-hash (saved-context theory)))
	  (postrestore-context *current-context*)
	      "Restored theory from ~a.bin in ~,2,-3fs (load part took ~,2,-3fs)"
	    filename (realtime-since start-time)
	    (floor (- load-time start-time) millisecond-factor))
	(progn (pvs-message "Bin file version for ~a is out of date"
	       (ignore-errors (delete-file file))
	       (dolist (thid *bin-theories-set*)
		 (remhash thid *pvs-modules*))
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools