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

Synopsis: rewriting after (ASSERT) throws away needed formula Severity: serious Priority: medium Responsible: shankar State: open Class: sw-bug Arrival-Date: Tue Mar 16 10:40:00 2004 Originator: "Ricky W. Butler" Organization: larc.nasa.gov Release: PVS 3.1 Environment: System: Architecture: Description: --=-7JQ9RhIePInWhFvtXYbr Content-Type: text/plain Content-Transfer-Encoding: 7bit Dear PVS: During the proof of B1 we observe the following behavior: Rule? (skosimp*) Repeatedly Skolemizing and flattening, this simplifies to: B1 : {-1} tr!1 > 0 {-2} 0 < TH {-3} ve!1`z = (H - s!1`z) / TH |------- {1} abs(s!1`z + (TH * ve!1)`z) >= H Rule? (assert) Simplifying, rewriting, and recording with decision procedures, this simplifies to: B1 : [-1] tr!1 > 0 [-2] 0 < TH [-3] ve!1`z = (H - s!1`z) / TH |------- {1} abs((TH * ve!1)`z + s!1`z) >= H Rule? (rewrite "cancel4") Found matching substitution: n0z: nonzero_real gets TH, y: real gets (H - s!1`z), x gets ve!1`z, Rewriting using cancel4, matching in *, this simplifies to: B1 : [-1] tr!1 > 0 [-2] 0 < TH |------- [1] abs((TH * ve!1)`z + s!1`z) >= H Notice that formula [-3] disappears. However, if we issue this rewrite command prior to the (assert) command this does not happen: Rule? (skosimp*) Repeatedly Skolemizing and flattening, this simplifies to: B1 : {-1} tr!1 > 0 {-2} 0 < TH {-3} ve!1`z = (H - s!1`z) / TH |------- {1} abs(s!1`z + (TH * ve!1)`z) >= H Rule? (rewrite "cancel4") Found matching substitution: n0z: nonzero_real gets TH, y: real gets (H - s!1`z), x gets ve!1`z, Rewriting using cancel4, matching in *, this simplifies to: B1 : [-1] tr!1 > 0 [-2] 0 < TH {-3} ve!1`z * TH = (H - s!1`z) |------- [1] abs(s!1`z + (TH * ve!1)`z) >= H Rule? Notice that {-3} is left in the sequent which is what is desired. In PVS 2.4 this does not happen. It seems to me that it is fine for the decision procedures to record this information, but the formula should not be removed, because further actions may be needed before it can be used. For example, see lemma B2 HH: real = H B2: LEMMA tr > 0 AND 0 < TH AND ve`z = (HH - s`z) / TH IMPLIES abs(s`z + (TH * ve)`z) >= H where there is a function in that formula that needs to be expanded before the proof will go through. Rick Butler P.S. The (cross-mult) strategy in the Manip package is seriously damaged by this change in PVS 3.1. Dozens of proofs were broken in our conflict and detection algorithm theories because of this. --=-7JQ9RhIePInWhFvtXYbr Content-Disposition: attachment; filename=BUG.dmp Content-Type: text/plain; name=BUG.dmp; charset=UTF-8 Content-Transfer-Encoding: 7bit %% PVS Version 3.1 %% 6.2 [Linux (x86)] (Feb 14, 2003 18:46) $$$bug.pvs bug: THEORY BEGIN Vect3 : TYPE = [# x,y,z:real #] a : VAR nonzero_real tr : VAR real vor : VAR Vect3 s : VAR Vect3 v,w : VAR Vect3 ve : VAR Vect3 *(a,w):Vect3=(# x:= a * w`x, y:= a * w`y, z:= a * w`z #) TH, H: real x, y: VAR real n0z : VAR nonzero_real cancel4: LEMMA x = y/n0z IFF x * n0z = y B1: LEMMA tr > 0 AND 0 < TH AND ve`z = (H - s`z) / TH IMPLIES abs(s`z + (TH * ve)`z) >= H HH: real = H B2: LEMMA tr > 0 AND 0 < TH AND ve`z = (HH - s`z) / TH IMPLIES abs(s`z + (TH * ve)`z) >= H END bug $$$bug.prf (bug (cancel4 0 (cancel4-1 nil 3288444502 3288444506 ("" (skosimp*) (("" (ground) nil nil)) nil) unchecked nil 3839 300 t shostak)) (B1_TCC1 0 (B1_TCC1-1 nil 3288433802 3288433961 ("" (subtype-tcc) (("" (postpone) nil nil)) nil) unfinished nil 66662 1750 t shostak)) (B1 0 (B1-1 nil 3288433967 3288444494 ("" (skosimp*) (("" (assert) (("" (rewrite "cancel4") (("" (postpone) nil nil)) nil)) nil)) nil) unfinished ((* const-decl "Vect3" bug nil) (H const-decl "real" bug nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (Vect3 type-eq-decl nil bug nil) (TH const-decl "real" bug nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (div_cancel4 formula-decl nil extra_real_props "Manip/") (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) 23807 970 t shostak)) (B2 0 (B2-1 nil 3288444683 3288444713 ("" (skosimp*) (("" (assert) (("" (rewrite "cancel4") (("" (expand "*") (("" (assert) (("" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) unfinished nil 30113 1400 t shostak))) --=-7JQ9RhIePInWhFvtXYbr-- How-To-Repeat: Fix:

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