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

PVS Bug 500


Synopsis:        Can prove FALSE with abstract-and-mc
Severity:        serious
Priority:        medium
Responsible:     shankar
State:           open
Class:           sw-bug
Arrival-Date:    Tue Dec  5 12:00:07 2000
Originator:      Martin Hofmann
Organization:    dcs.ed.ac.uk
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  Dear PVS developers,
  
  We have "succeeded" in proving FALSE in the empty context using
  abstract-and-mc. See below for the offending theory and proof script. 
  We have been using the following version:
  
      PVS Version 2.3 (patch level 1.2.2.36)
  
  	Please check our website periodically for news of later versions
  			   at http://pvs.csl.sri.com/
  
  			Allegro CL Professional Edition
  			 5.0 [Linux/X86] (9/4/99 13:27)
  
  If this problem has already been reported or addressed we would
  appreciate info about patches!
  
  Francis Tang and Martin Hofmann
  
  
  
  -----------------------------------------------------
  a.pvs:
  ----------------------------------------------------
  a:THEORY
  
  BEGIN
  
  L : TYPE = {u,v,w,z}
  H : TYPE ={t,b}
  Q : TYPE = [#label:L, layer:H, dummy:int #]  % model-check fails here 
  
  
  initial(x:Q):bool = (x`label = u AND x`layer=b)
  final(x:Q):bool = (x`label = z AND x`layer=t)
  
  R(x,y:Q) : bool = (
       x`label=u AND y = x WITH[label := v]
    OR x`label=v AND y=x
  %  OR x`label=u AND x`layer=t AND y=x WITH [label:=w]
    OR x`layer=b AND y=x WITH [layer := t]
    OR x`label=w AND x`layer=t AND y = x WITH [label := z])
  
  
  th : THEOREM FORALL(x:Q):initial(x) IMPLIES mu(LAMBDA(q:pred[Q]):final OR EX(
 R,q))(x)
  
  P(x:Q):bool = x`label=w OR x`label=z
  
  lem:THEOREM FORALL (x:Q):mu(LAMBDA(q:pred[Q]):final OR EX(R,q))(x) IMPLIES P(
 x)
  
  lem2:THEOREM FORALL (x:Q):initial(x)IMPLIES final(x)
  
  lem3:THEOREM FALSE
  
  END a
  
  ---------------------------------------------------------------------------
  a.prf
  ----------------------------------------------------------------------------
  (|a|
   (|th| ""
    (ABSTRACT-AND-MC
     ("LAMBDA(x:Q):x`label=u OR x`label=v" "LAMBDA(x:Q):x`label=u OR x`label=w"
      "LAMBDA(x:Q):x`layer=b"))
    NIL NIL)
   (|lem| "" (SKOSIMP)
    (("" (EXPAND "mu")
      (("" (EXPAND "lfp")
        (("" (EXPAND "glb")
          (("" (INST -1 "P")
            (("" (SPLIT -1)
              (("1" (PROPAX) NIL NIL)
               ("2" (DELETE 2) (("2" (GRIND) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|lem2| "" (SKOSIMP)
    (("" (LEMMA "th") (("" (LEMMA "lem") (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL
 )
   (|lem3| "" (LEMMA "lem2")
    (("" (INST -1 "(#label:=u,layer:=b,dummy:=0#)") (("" (GRIND) NIL NIL)) NIL)
 )
    NIL))

How-To-Repeat: 

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