Home | • | Intro | • | Announce | • | FAQ | • | Docs | • | Download | • | • | Status | • | Bugs | • | Users | • | Related | • | FM Tools |
---|

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 | • | • | Status | • | Bugs | • | Users | • | Related | • | FM Tools |
---|