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

PVS Bug 510


Synopsis:        Importing nonexisting theories
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Mon Jan  8 10:40:05 2001
Originator:      Hendrik Tews
Organization:    inf.tu-dresden.de
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  typecheck the following file
  
      % TC although A is not available
  
      A : Theory Begin End A
  
      B : Theory Begin IMPORTING A End B
  
  change it then into 
  
      % TC although A is not available
  
      %A : Theory Begin End A
  
      B : Theory Begin IMPORTING A End B
  
  and type C-c C-t again. PVS does not produce an error although
  theory A is not available in the context.
  
  Bye,
  
  Hendrik
  

How-To-Repeat: 

 [davesc]
 Fixed. See also bug # 556, reporting the same issue.

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