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

PVS Bug 784


Synopsis:        rule-induct fails on Coinductive definitions
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Fri Jun 20 04:30:01 2003
Originator:      Hendrik Tews
Organization:    tcs.inf.tu-dresden.de
Release:         PVS 3.1
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  the subject says everything. Aparently rule-induct looks for
  something in the antecedents, while for coinductive definitions
  it should search the consequents.
  
  Bye,
  
  Hendrik

How-To-Repeat: 

Fix: 
Modified rule-induct and rule-induct-step to allow for coinductive relations.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools