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

PVS Bug 634


Synopsis:        Declarations in assumptions rejected
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Wed Dec 12 03:05:00 2001
Originator:      Hendrik Tews
Organization:    tcs.inf.tu-dresden.de
Release:         PVS 2.4
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  the following theory typechecks in 2.3 but is rejected in 2.4:
  
      A[ B : Type] : Theory
      Begin
        Assuming
  	myid : [B -> B] = lambda(b:B) : b
  	id_comp : Assumption myid o myid = myid
        EndAssuming
      End A
  
  The error says 
     Error: assumption refers to myid, which would not be visible in
     the associated TCC 
  
  
  Is this a bug or a feature? Assuming it is a feature I looked at
  "6.5 Assuming Part" of the language reference. However I could
  not spot any difference with the 2.3 documentation.
  
  
  Bye,
  
  Hendrik
  

How-To-Repeat: 

Fix: 
The language document has been updated, in the course of which it was
discovered that this error is not quite correct, as it is OK if the theory
with assumings (A in this case) is first imported generically.

Hence modified generate-assuming-tccs to check for nonvisible
references in the assumptions, and complain if there are any.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools