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
Environment: 
 System:          
 Architecture: 

Description: 
  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
   BEGIN
  
    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
         (implicit-conversion)
    [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/

How-To-Repeat: 

Fix: 
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)))
			   'prelude-declarations-hash)))
	  (postrestore-context *current-context*)
	  (pvs-message
	      "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))
	  theory)
	(progn (pvs-message "Bin file version for ~a is out of date"
		 filename)
	       (ignore-errors (delete-file file))
	       (dolist (thid *bin-theories-set*)
		 (remhash thid *pvs-modules*))
	       nil))))
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools