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

PVS Bug 870


Synopsis:        Error: the assertion (new in 3.2)
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Tue Nov 23 02:50:00 2004
Originator:      Hendrik Tews
Organization:    tcs.inf.tu-dresden.de
Release:         PVS 3.2
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  status-proof-chain crashes on pattern_type_correct_body_1 in
  programms-4 after typechecking. 
  
  This bug is new in 3.2.
  
  I would appreciate any patches or hints for work-arounds.
  
  Bye,
  
  Hendrik

How-To-Repeat: 

Fix: 
This was due to a recent change made to the way the proofchain is
displayed, as it used to simply list the results from a hash table, which
is a fairly random order.  The sorting algorithm tries to take into
account theories and libraries, and it was an incompleteness here that
caused the assert error.

(defun pc-sort (decls &optional theory)
  (assert (or theory *current-context*))
  (let* ((th (or theory (current-theory)))
	 (imps (cons th (complete-importings th))))
    (assert (every #'(lambda (x)
		       (or (from-prelude? x)
			   (from-prelude-library? x)
			   (memq (module x) imps)))
		   decls))
    (sort decls
	  #'(lambda (x y)
	      (cond ((eq (module x) (module y))
		     (string< (id x) (id y)))
		    ((from-prelude? y)
		     (or (not (from-prelude? x))
			 (string< (id (module x)) (id (module y)))))
		    ((from-prelude-library? y)
		     (and (not (from-prelude? x))
			  (or (not (from-prelude-library? x))
			      (string< (id (module x)) (id (module y))))))
		    (t (and (not (from-prelude? x))
			   (memq (module y) (memq (module x) imps)))))))))

(defun complete-importings (th)
  (multiple-value-bind (imps impnames)
      (all-importings th)
    (multiple-value-call #'add-generated-interpreted-theories
			 (add-generated-adt-theories
			  (cons th imps)
			  (cons (mk-modname (id th)) impnames))
			 th)))

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