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

PVS Bug 563


Synopsis:        error message missing with inst for nested forall
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Tue May 15 02:55:00 2001
Originator:      Hendrik Tews
Organization:    tcs.inf.tu-dresden.de
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  consider the following theory
  
      A : Theory
      Begin
        a : Lemma not Forall(n : nat): Forall(m:nat) : n = m
      end A
  
  when I start the proof of a with (INST -1 "4" "n") I get
  
      Instantiating the top quantifier in -1 with the terms: 
       4, n,
      this simplifies to: 
      a :  
  
      {-1}  FORALL (m: nat): 4 = m
        |-------
  
  Instead of an error 
  
      Expecting an expression
      No resolution for n
  
  
  Bye,
  
  Hendrik
  

How-To-Repeat: 

Fix: 
Modified inst to fail if the recursive call doesn't succeed.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools