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

PVS Bug 466


Synopsis:        Incorrect proof-incomplete status
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Tue Jun 27 15:20:03 2000
Originator:      Jonathan Ford
Organization:    turing.une.edu.au
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  
  Some of the TCCs are marked proved - incomplete, but these have been
  proved with either a SUBTYPE-TCC, or a GRIND rule. All of these TCCs have
  something of the form:
  
  length(L) = length(M) IMPLIES
    FORALL (i: below[length(L)]):
      i < length(M)
  
  Where L and M are lists. Can you tell us why this is the case?

How-To-Repeat: 

Fix: 

Proofchain analysis does a check for circularity (mostly as a sanity
check, as it should not happen), and incorrectly decided that the use of
an inductive definition was circular.  Fixed pc-analyze* (declaration)
accordingly.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools