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

PVS Bug 1006


Synopsis:        bound variables clash
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Fri Sep 28 09:30:00 2007
Originator:      Hesselink
Organization:    rug.nl
Release:         PVS 4.0
Environment: 
 System:          
 Architecture: 

Description: 
  This is a multi-part message in MIME format.
  --------------090004000208000108030400
  Content-Type: text/plain; charset=ISO-8859-1; format=flowed
  Content-Transfer-Encoding: 7bit
  
  Dear Sam,
  
  I am getting a clash of bound variables. The lemma asserts that every 
  natural number is followed eventually by an odd one, but it turns out to 
  be nonprovable. See dump.
  
  Best regards,
  Wim
  
  -- 
                          Wim H. Hesselink  
  
   Dept. of Computing Science       /   phone +31 50 3633933
      University of Groningen      /       or +31 50 3633939
                  P.O.Box 407     /     fax   +31 50 3633800
            9700 AK Groningen    /      email: w.h.hesselink@rug.nl
              The Netherlands   /       http://www.cs.rug.nl/~wim
  
  
  --------------090004000208000108030400
  Content-Type: text/plain;
   name="boundvarsDump"
  Content-Transfer-Encoding: 7bit
  Content-Disposition: inline;
   filename="boundvarsDump"
  
  
  %% PVS Version 4.0 - Allegro CL Enterprise Edition 8.0 [Mac OS X (Intel)] (No
 v 28, 2006 15:57)
  %% 8.0 [Mac OS X (Intel)] (Nov 28, 2006 15:57)
  $$$errprop.pvs
  errprop:  THEORY
  
  BEGIN
    xs: VAR sequence[nat]
    i, n: VAR nat
  
    p: VAR pred[sequence[nat]]
  
    suffix(xs, n): sequence[nat] =
      LAMBDA i: xs(n+i)
  
    box(p): pred[sequence[nat]] =
      {xs | FORALL n: p(suffix(xs, n))}
  
    NOT(p): pred[sequence[nat]] =
      {xs | NOT p(xs)}
  
    diamond(p): pred[sequence[nat]] =
      NOT (box (NOT (p)))
  
    odd(xs): bool =
      EXISTS i: xs(0) = 2*i+1
  
    lem: LEMMA
      box(diamond(odd))(id)
  
  END errprop
  
  $$$errprop.prf
  (errprop
   (lem 0
    (lem-1 nil 3399971611 3399972610
     ("" (expand "diamond")
      (("" (expand "NOT")
        (("" (expand "box")
          (("" (expand "suffix")
            (("" (expand "id")
              (("" (skosimp)
                (("" (expand "odd")
                  (("" (inst - "1") (("" (postpone) nil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     unfinished nil 999043 90 t shostak)))
  
  
  --------------090004000208000108030400--

How-To-Repeat: 

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