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

PVS Bug 508


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

Description: 
  Hi,
  
  Consider the following theory:
  
      A : Theory
      Begin
        f(n : nat) : nat = 1
  
        a : Lemma 
  	    (Lambda(h : [nat -> nat]) : Forall(f : [nat -> nat]) : h = f) (f)
      end A
  
  invoke a proof on a and do assert, this yields
  
      a :  
  
        |-------
      {1}   FORALL (f: [nat -> nat]): f = f
  
  In this sequent the bound variable f and the constant f are mixed
  up. Internally they are still different (as (expand "f")
  demonstrates). 
  
  I consider the capture of the constant a bug, because the printed
  sequent is a tautology, whereas the internal version is false. At
  least the output of M-x show-expanded-sequent should be in 1-1
  correspondence with the internal representation.
  
  Bye,
  
  Hendrik
  

How-To-Repeat: 

Fix: 
Fixed substit to check for capture of a constant.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools