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

# PVS Bug 829

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