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

PVS Bug 404


Synopsis:        BUGS in PVS 2.3 beta
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Tue Aug 03 16:18:03 1999
Originator:      "Ralph D. Jeffords"
Organization:    itd.nrl.navy.mil
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  ----------
  X-Sun-Data-Type: text
  X-Sun-Data-Description: text
  X-Sun-Data-Name: text
  X-Sun-Charset: us-ascii
  X-Sun-Content-Lines: 1
  
  Description of TWO problems in attached .dmp file
  ----------
  X-Sun-Data-Type: default
  X-Sun-Data-Description: default
  X-Sun-Data-Name: bug_subtype.dmp
  X-Sun-Charset: us-ascii
  X-Sun-Content-Lines: 58
  
  
  $$$bug_subtype.pvs
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  % (1) Bug in subtype:
  %
  % PVS 2.3 beta gets confused about the definition of f
  % and returns the following message
  %
  % f does not uniquely resolve - one of:
  %
  %  bug_subtype.f : [rec -> nat],
  %
  %  bug_subtype.f : [rec -> nat]
  %
  % Leaving out the "R: VAR rec" below makes the problem
  % go away  (No problems with this example in PVS 2.2 )
  %
  %--------------------------------------------------------
  % (2) Bug???? in dump-pvs-files:
  %
  % If the bug_subtype_rec theory is imported from another
  % file (say bug_subtype_rec.pvs) then dump-pvs-files
  % does NOT include it in the dump. This appears to happen
  % because the theory does NOT type-check (PVS 2.2 has the
  % same behavior if a typecheck error is found). Shouldn't
  % the dump-pvs-files command try to dump all imported
  % files even if type-check fails????
  %
  % 3 aug. 1999
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
  
  bug_subtype_rec: THEORY
  BEGIN
  
  rec: TYPE = [# f: nat #]
  
  	R: VAR rec
  
  sub?(R):boolean
  
  END bug_subtype_rec
  
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
  bug_subtype: THEORY
  BEGIN
  	IMPORTING bug_subtype_rec
  
  rec:TYPE = [# f: nat #]
  
  	R: VAR rec 	% Leave this out to fix the problem
  
  main: THEOREM
  
  	FORALL (R: (sub?)): f(R) = f(R)
  
  END bug_subtype

How-To-Repeat: 


Fix: 

 [dave_sc, 4/16/01]
 Confirmed part (1) is fixed in 2.3 with latest patches.

 Part (2) is a little more tricky - how to establish what files
 constitute the importing hierarchy if it won't typecheck.  Will
 discuss with Sam.

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