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

PVS Bug 1050


Synopsis:        misleading error message
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Tue Apr 13 02:35:01 -0700 2010
Originator:      Hendrik Tews
Release:         PVS 4.2
Organization:    os.inf.tu-dresden.de
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  for the appended spec (identical to the one in bug report #511)
  PVS reports
  
      Incompatible types for same_domain?(R)
  	 Found: lift_adt[boolean].lift
        Expected: booleans.boolean
  
  for the the same_domain? in the last lemma. However, same_domain?
  is clearly declared as boolean.
  
  If one accepts the wrong type PVS derives and changes the last
  lemma, for instance, in 
  
    percl_rel_prod_coll : Lemma same_domain?(R) = up(true)
  
  PVS reports the true problem with 
  
      Could not determine the full theory instance for same_domain?
  
  Bye,
  
  Hendrik
  
  
  ==================== specification ================================
  
  Collection[Base, Index : Type] : Theory
  Begin
    collection : Type = [Index -> PRED[Base]]
  
    Coll_or(c : collection) : PRED[Base] =
      Lambda(b : Base) : Exists(i : Index) : c(i)(b)
  end Collection
  
  PReflexive[A : Type] : Theory
  Begin
  
    R : Var PRED[[A,A]]
  
     domain(R) : PRED[A] = Lambda(a:A) : Exists(b:A) : R(a,b) or R(b,a)
  
  end PReflexive
  
  PerCollection[A,C : Type] : Theory
  Begin
    IMPORTING PReflexive[A], Collection
  
    R : Var collection[[A,A], C]
  
    domain(R) : PRED[A] = domain(Coll_or(R))
  
    same_domain?(R) : bool = Forall(i:C) : domain(R(i)) = domain(R)
  
  End PerCollection
  
  PerUnion[X, Y, C : Type] : Theory
  Begin
    IMPORTING PerCollection
  
    R : Var collection[[X,Y], C]
  
    percl_rel_prod_coll : Lemma same_domain?(R)
  
    %percl_rel_prod_coll : Lemma same_domain?(R) = up(true)
  
  End PerUnion

How-To-Repeat: 

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