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

PVS Bug 769


Synopsis:        Unexpected restrict of numfield type
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Fri May  2 16:40:01 2003
Originator:      Alfons Geser
Organization:    shrimp.nianet.org
Release:         PVS 3.1
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  an unexpected "restrict" is produced in PVS 3.1. The code works
  perfectly with PVS 2.4.
  
  Alfons
  
  ---
  
  Attempting to prove lemma t1 by
  
  (skosimp*) (expand "form_set") (expand "singleton") (assert)
  
  produces the sequent
  
  [-1]  restrict[[# te: numfield, ve: Vect3, vr: Vect3 #], solution, boolean]
            ({y: [# te: numfield, ve: Vect3, vr: Vect3 #] |
                y =
                 (# ve := put_z(v!1, vez!1),
                    vr := put_z(v!1, vrz!1),
                    te
                      := (v!1(2) * tr!1 - tr!1 * vrz!1) / (vez!1 - vrz!1) #)})
            (m!1)
    |-------
  {1}   m!1 =
         (# ve := put_z(v!1, vez!1),
            vr := put_z(v!1, vrz!1),
            te := (v!1(2) * tr!1 - tr!1 * vrz!1) / (vez!1 - vrz!1) #)
  
  which seems unprovable.  If "singleton" is qualified by "[solution]"
  (as in the commented line) then the proof works.
  
  ---
  
  %% Unexpected restrict of numfield type
  
  restrict_bug: THEORY
  BEGIN
  
    IMPORTING vectors@vect3D
  
    solution : TYPE = [# ve: Vect3, vr:Vect3, te:real #]
    
    v   : VAR Vect3
    tr, te, vez, vrz  : VAR real
    m   : VAR solution
  
    form_set(v, vez, vrz, tr) : set[solution] =
  %        singleton((# ve:= put_z(v, vez),
          singleton[solution]((# ve:= put_z(v, vez),
                       vr:= put_z(v, vrz),
                       te:= tr*(z(v) - vrz)/(vez-vrz) #))
  
    t1 : LEMMA
        form_set(v, vez, vrz, tr)(m)
      IMPLIES
        m = (# ve:= put_z(v, vez),
               vr:= put_z(v, vrz),
               te:= tr*(z(v) - vrz)/(vez-vrz) #)
  
  END restrict_bug

How-To-Repeat: 

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