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

PVS Bug 564


Synopsis:        (typepred "<") breaks prover
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Tue May 15 02:55:01 2001
Originator:      Joachim van den Berg
Organization:    cicero.cs.kun.nl
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  Dear PVS-developers,
  
  at the end of this email you can find a (nonsense) example that breaks the
  prover when (typepred "<") is given as rule. I've reduced the problem I had
  to example as included below. The problem occurs for the patch levels
  1.2.2.146 and 1.2.2.150. The patch level 1.2.2.127 didn't give rise to any
  problems.
  
  A workaround for this problem is to use
    (typepred "Bug.<::(well_founded?[A])")
  instead. 
  
  I running PVS on a RedHat Linux 7.0 machine with (x)emacs.
  
  Best,
  Joachim van den Berg
  _____________________________________________________________
    Joachim van den Berg___________________tel. +31 24 36 52710
    Computer Science Institute_________mailto:joachim@cs.kun.nl
    University of Nijmegen_______http://www.cs.kun.nl/~joachim/
  
  --
  Bug[A : TYPE+, < : (well_founded?[A])] : THEORY
  BEGIN
  
    < : PRED[[nat, nat]] = LAMBDA(x : [nat,nat]) : TRUE
  
    % (skosimp)
    % (typepred "<")  breaks the prover
    % (typepred "Bug.<::(well_founded?[A])")
    foo : LEMMA
      FORALL (n : posnat) : 0 < n
  
  END Bug
  

How-To-Repeat: 

Fix: 
This was fixed for a related bug.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools