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