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

PVS Bug 945


Synopsis:        PVS 3.3 release candidate testing
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Tue Jan 24 13:45:00 2006
Originator:      "Ricky W. Butler"
Organization:    larc.nasa.gov
Release:         PVS 3.2
Environment: 
 System:          
 Architecture: 

Description: 
  Sam,
     I have begun testing the PBS 3.3 beta with our libraries.  Here is a
  problem I found in the "reals" library.
  
  If you rerun lemma "harmonic_polynomial_real_rec" in the
  harmonic_polynomials theory you will encounter subgoals such as
  
    harmonic_polynomial_real_rec.1.1.1.1.1.1.2.1 :  
  
    {-1}  0 >= 0
    {-2}  i!1 = 0
    |-------
    {1}   real_pred(F2(0))
  
  If you issue command (reveal -2) you get 
  
  
  {-1}  (LAMBDA (i_1: nat):
           x *
            (LAMBDA (i_1: nat):
               IF i_1 > n OR odd?(i_1) THEN 0
               ELSE C(n, i_1) * (-1) ^ (i_1 / 2) *
                     (IF i_1 = 0 THEN x ^ n
                      ELSIF i_1 = n THEN y ^ n
                      ELSE x ^ (n - i_1) * y ^ i_1
                      ENDIF)
               ENDIF)
                (i_1))
         = F2
  [-2]  0 >= 0
  [-3]  i!1 = 0
    |-------
  [1]   real_pred(F2(0))
  
  
  If you try command (replace -1 * RL) nothing happens.
  
   (replace -1 * RL)
    No change on: (replace -1 * RL)
  
  The system should know that F2(0) is an integer and hence real
  but does not.
  
  There are several more subgoals with this same problem.
  
  Rick
  

How-To-Repeat: 

Fix: 
This is the same bug as #935, and has been fixed.  The problem is that the
prover is now case-sensitive, and RL was being quietly ignored (as would
any invalid entry).  The fix now allows any case for lr or rl, and
complains for invalid values.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools