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

PVS Bug 469


Synopsis:        Data-Subtypes
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Fri Jul  7 14:20:01 2000
Originator:      "Sylvan S. Pinsky"
Organization:    thematrix.ncsc.mil
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  --Blessing_of_Unicorns_123_000
  Content-Type: TEXT/plain; charset=us-ascii
  Content-MD5: Y8AYbLLYkws/6VPWtck4Ww==
  
  Hi Sam,
  
  I have a simple question regarding lists of data-subtypes.  I developed a
  datatype called object with subtypes obj and method (see attached file).
  
  The datatype subst defined by
  
        subst: DATATYPE 
                BEGIN
                 SCONS(SKEY:vr, SENTRY:obj, SNEXT:subst): is_SCONS?
                 SNIL: is_SNIL?
                END subst
                
  is essentially the same as a list of (vr,obj) pairs; however, they
  behave differently when used in recursive functions.
  
  Define pr: TYPE = [vr,obj] with the object ob, the subst s, and the list[pr] 
 X.
  
  Substitutions for the method fct(x,o) using s and a change of variables
  involves SUB(o,SCONS(x,ovar(new(o)),s)) which generates no tccs.
  
  When using X in SUB(o,cons((x,ovar(new(o))),X) a tcc is generated for the
  list cons((x,ovar(new(o))),X); namely,
  
  SUBLLST_TCC5: OBLIGATION
    FORALL (O: obj, x: vr, X, ob):
     ob = fct(x, O) IMPLIES
      every[[vr, object]]
        (LAMBDA (t: [vr, object]): is_ovar?(t`2) OR is_comb?(t`2))
        (cons[[vr, object]]((x, ovar(new(O))), X));
        
  The tcc is easy enough to prove.  I was just curious as to why it is 
  generated?  Is it because the type [vr, obj] is a data-subtype of [vr, object
 ]
  and lists are compound structures?
  
  Why does the list require a tcc, yet the essentially equivalent subst 
  structure doesn't?
  
  Regards,
  
  Sylvan

  ---spec removed---

How-To-Repeat: 

Fix: 
Hi Sylvan,

That's an interesting experiment.  It took me a little while
to realize what was going on.  Although subst and list have
the same structure, the fact that list has a positive type
parameter changes things.  This is what allows, e.g.,
list[nat] to be viewed as a subtype of list[int]:

  list[nat] is equivalent to {x: list[int] | every(LAMBDA (i:int): i >= 0)(x)}

In your case, the type of X is actually
 {x: list[[vr,object]] |
      every(LAMBDA (t: [vr, object]): is_ovar?(t`2) OR is_comb?(t`2))(x)}

When the typechecker has to determine the type of the cons in
cons((x,ovar(new(o))),X), it needs to lift it to a higher
type.  Thus [vr, (is_ovar?)] is lifted to [vr, object].  I
looked into this, and realized that it really should be lifted
to [vr, obj], and that the reason it skips this is that the
typechecker doesn't directly "know" that (is_ovar?)  is a
subtype of obj.  To test this hypothesis out, I added the
judgement

   JUDGEMENT (is_ovar?) SUBTYPE_OF obj

and the TCC disappeared.  I'm going to fix things so that such
judgements are automatically generated when datatypes with
subtypes are typechecked.

Thanks for bringing this to my attention.

Regards,
Sam
--------

Fixed generate-adt-subtypes (datatype-with-subtypes) to generate subtype
judgements for those subtypes with more than one recognizer.

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