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

PVS Bug 963


Synopsis:        Minor bug in (induct "i") using nat_induction
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Tue Sep 26 19:30:00 2006
Originator:      "Ralph D. Jeffords"
Organization:    itd.nrl.navy.mil
Release:         PVS 3.2
Environment: 
 System:          
 Architecture: 

Description: 
  %================================================
  % BUG in (induct "i") that uses nat_induction
  %
  %  Versions:    2.4  patchlevel 1  on Sun Solaris
  %        3.2  beta          on Sun Solaris
  %
  % Ralph D. Jeffords, Naval Research Lab
  % 26 sep 2006
  %================================================
  bug_nat_induction: THEORY
  
  BEGIN
  
  State: TYPE+
  
     i: VAR nat
     j:  nat
     s: sequence[State]
        P,Q: [State -> boolean]
  
  %------------------------------------------------------------------
  % (induct "i") results in 4 subgoals  with some extra formulas that
  % are garbage and one of the subgoals repeated???
  %
  %
  %   |-------
  % {1}   P(s(0))
  %
  %
  % {-1}  Q(s(0))
  %   |-------
  % {1}   P(s(i!1)) <-----GARBAGE
  %
  %
  %
  % {-1}  Q(s(i!1)) <------GARBAGE   \
  % {-2}  Q(s(0))                     > REPETITION OF PREVIOUS SUBGOAL
  %   |-------                       /
  %
  %
  %   |-------
  % {1}   FORALL j: P(s(j)) & NOT Q(s(j)) IMPLIES P(s(j + 1)) & NOT Q(s(j 
  + 1))
  %
  %
  % This bug cropped up in rerunning some old proofs that were about 10 
  years old
  % ---I don't know what version of PVS these were run under originally but I
  %  would guess some Version 1 release. From the proof scripts it seems 
  the old
  %  (induct "i") resulted in three subgoals:
  %
  %
  %   |-------
  % {1}   P(s(0))
  %
  %
  % {-1}  Q(s(0))
  %   |-------
  % {1}   %
  %
  %   |-------
  % {1}   FORALL j: P(s(j)) & NOT Q(s(j)) IMPLIES P(s(j + 1)) & NOT Q(s(j 
  + 1))
  %
  %
  %----------------------------------------------------------------------------
 -
  
  main: THEOREM
  
     FORALL i:  P(s(i)) & NOT Q(s(i))
  
  
  END bug_nat_induction

How-To-Repeat: 

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