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

PVS Bug 873


Synopsis:        TCC pretty printing problem
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Wed Nov 24 15:40:00 2004
Originator:      Hendrik Tews
Organization:    tcs.inf.tu-dresden.de
Release:         PVS 3.2
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  PVS generates the following TCC in utility.pvs in the appended
  archive:
  
    nth_flatten_TCC1: OBLIGATION
      FORALL (ll: list[list[T]], m: nat, n):
        m < length(nth(ll, n)) AND n < length(ll) IMPLIES
         add_list(take[nat](map[list[T], nat](length[T])(ll), n)) + m <
  	length[T](flatten(ll));
  
  I would have expected
  
  nth_flatten_TCC1: OBLIGATION
    FORALL (ll: list[list[T]], n, m: nat,):
                              ^^^
      n < length(ll) AND m < length(nth(ll, n)) IMPLIES
      ^^^^^^^^^^^^^^     ^^^^^^^^^^^^^^^^^^^^^^
       add_list(take[nat](map[list[T], nat](length[T])(ll), n)) + m <
        length[T](flatten(ll));
  
  Bye,
  
  Hendrik

How-To-Repeat: 

Fix: 
The function add-tcc-bindings should reverse the antes and bindings
arguments before applying them.

(defun add-tcc-bindings (expr conditions substs antes &optional bindings)
  (if (typep (car conditions) 'bind-decl)
      ;; Recurse till there are no more bindings, so we build
      ;;  FORALL x, y ... rather than FORALL x: FORALL y: ...
      (let* ((bd (car conditions))
	     (nbd (or (cdr (assq bd substs)) bd)))
	(add-tcc-bindings expr (cdr conditions) substs antes
			  (if (or (occurs-in bd expr)
				  (occurs-in bd antes)
				  (occurs-in bd substs)
				  (possibly-empty-type? (type bd)))
			      (cons nbd bindings)
			      bindings)))
      ;; Now we can build the universal closure
      (let* ((nbody (substit (if antes
				 (make!-implication
				  (make!-conjunction* (reverse antes))
				  expr)
				 expr)
		      substs))
	     (nbindings (get-tcc-closure-bindings bindings nbody))
	     (nexpr (if nbindings
			(make!-forall-expr (reverse nbindings) nbody)
			nbody)))
	(add-tcc-conditions* nexpr conditions substs nil))))
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools