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

PVS Bug 551


Synopsis:        Unprovable TCC for theory actual
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Mon Apr  2 15:50:00 2001
Originator:      Christoph Berg
Organization:    cs.uni-sb.de
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  
  
  Hello,
  
  in the following PVS file, an unprovable TCC is generated for the second
  lemma, whereas both lemmas should be equivalent.
  
  -------8<-------
  anyfunction[x: real]: theory
  begin
    anyfunction: real =3D 0
  end anyfunction
  
  nonzerofunc: theory
  begin
    nonzerofunc(x: nonzero_real): real
  end nonzerofunc
  
  nonzerotcc: theory
  begin
    importing anyfunction, nonzerofunc
  
    % this lemma is ok:
    nonzero_lemma_ok: lemma
      forall (x: real):
        x /= 0 implies
          let xx = nonzerofunc(x) in anyfunction[xx] = 0
  
    % the following lemma generates an unprovable TCC:
    % nonzerolemma_TCC1: OBLIGATION FORALL (x: real): x /= 0
    nonzerolemma: lemma
      forall (x: real):
        x /= 0 implies
          anyfunction[nonzerofunc(x)] =3D 0
  
  end nonzerotcc
  -------8<---------
  
   Proof summary for theory anyfunction
      Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
  
   Proof summary for theory nonzerofunc
      Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
  
   Proof summary for theory nonzerotcc
      nonzero_lemma_ok............................proved - complete   [O](0.0=
  2 s)
      nonzerolemma_TCC1...........................unfinished          [O](0.0=
  7 s)
      nonzerolemma................................proved - incomplete [O](0.0=
  1 s)
      Theory totals: 3 formulas, 3 attempted, 2 succeeded (0.10 s)
  
  Grand Totals: 3 proofs, 3 attempted, 2 succeeded (0.10 s)
  
  Christoph Berg


How-To-Repeat: 

 [dave_sc]  See also b295

 [7/18, dave_sc]
 Ok now, due to recent updates in the typechecker the TCC
 is no longer generated.

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