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

PVS Bug 876


Synopsis:        Theory interpretations in PVS3.2
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Mon Nov 29 11:20:00 2004
Originator:      "Cesar A. Munoz"
Organization:    nianet.org
Release:         PVS 3.2
Environment: 
 System:          
 Architecture: 

Description: 
  I have discovered a family of errors related to typechecking of theory
  interpretations in PVS3.2:
  
  Assume:
  
  quadratic : theory
  begin
   
    sqrt_ax(x:nnreal): {y:nnreal | y*y = x}
   
  end quadratic
  
  quadratic_io : theory
  begin
   
    SQRT : [nnreal->nnreal]
   
    quio : theory = quadratic{{sqrt_ax := SQRT}}
   
  end quadratic_io
  
  1. Typechecking quadratic_io yields:
  Illegal reference to SQRT
  May not use theory declarations with actuals or mappings that reference
  entities declared in this theory.
  
  2. Change the declaration of SQRT to   
  SQRT : [real->nnreal]
  
  The typechecker returns:
  Error: No methods applicable for generic function
  
  3. Delete the declaration of SQRT. Load the PVSio library that defines
  SQRT. Then, the file typechecks correctly. Exit PVS, load PVS,
  typechecking the file a second time results in:
  
  Error: the assertion (filename theory) failed.
  
  Cesar
  PS. The second problem is probably related to:
  http://www.csl.sri.com/cgi-bin/pvs/pvs-bug?id=866
  
  -- 
  Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
  National Institute of Aerospace      mailto://C.A.Munoz@larc.nasa.gov
  144 Research Drive                  http://research.nianet.org/~munoz
  Hampton, VA 23666, USA   Tel. +1 (757) 766 1539 Fax +1 (757) 766 1855
  

How-To-Repeat: 

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