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

PVS Bug 711


Synopsis:        Multiple proofs and proof display in PVS3
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Thu Aug 22 20:35:01 2002
Originator:      Bruno Dutertre
Organization:    sdl.sri.com
Release:         PVS 2.4
Environment: 
 System:          
 Architecture: 

Description: 
  This is a multi-part message in MIME format.
  --------------040206000906060002020401
  Content-Type: text/plain; charset=us-ascii; format=flowed
  Content-Transfer-Encoding: 7bit
  
  Sam,
  
  The show-proofs- comands show the axioms
  in a theory as [untried] rather than hide them
  as before. The display-proofs- commands
  do the same thing, they show status `nil'
  for the axioms.
  
  In some cases, empty proofs are kept around.
  Although I always answered yes when PVS asked
  if I wanted the previous proof overwritten,
  some formulas in the attached theory have
  several proofs. For example, display-proof-formula
  for finite_leave_requests  shows two proofs,
  one of which is `nil'.
  
  I don't know exactly how to reproduce this, but
  it seems to be related to typechecking.
  
  Bruno

----spec removed------

How-To-Repeat: 

Fix: 
The empty proofs act as placeholders, but were not properly recognized.
This has been fixed in the prover and the various display functions.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools