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

PVS Bug 868


Synopsis:        TCC generation bug
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Fri Nov 19 00:50:00 2004
Originator:      Pertti Kellomaki
Organization:    cs.tut.fi
Release:         PVS 3.2
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  Typechecking the following theory in PVS 3.2 gives only one TCC
  instead of the expected two:
  
  ----------------------------------------------------------------------
  bug : THEORY
    BEGIN
  
    p(fn  : [nat -> nat]) : bool = forall (a : nat) : fn(a) < 10
  
    f : [nat -> nat] = (lambda (aa : nat) : 10)
    g : [nat -> nat] = f WITH [(0) := 1]
  
    tst_T : TYPE = [# n : (p) #]
  
    tst_v1 : tst_T = (# n := g #)
    tst_v2 : tst_T = (# n := f WITH [(0) := 1] #)
  
    END bug
  ----------------------------------------------------------------------
  
  The (unprovable) TCC that gets generated is
  
      % Subtype TCC generated (at line 11, column 27) for  g
          % expected type  (p)
  	  % unfinished
      tst_v1_TCC1: OBLIGATION p(g);
  
  No TCC is generated for tst_v2. This is an improvement over PVS 3.1,
  though, as no TCCs at all are generated there.
  
  Regards,
  	Pertti

How-To-Repeat: 

Fix: 
Modified set-assignment-arg-types* (subtype) to call check-for-subtype-tcc
rather than set-type*

(defmethod set-assignment-arg-types* (args-list values ex (expected subtype))
  (typecase (find-supertype expected)
    ((or funtype recordtype tupletype adt-type-name)
     (set-assignment-arg-types* args-list values ex (supertype expected))
     (mapc #'(lambda (a v)
	      (unless a (check-for-subtype-tcc v expected)))
	   args-list values))
    (t (call-next-method))))
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools