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

PVS Bug 631


Synopsis:        BUG: (apply-extensionality) on function overrides
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Tue Dec 11 13:20:01 2001
Originator:      Ralph D. Jeffords
Organization:    itd.nrl.navy.mil
Release:         PVS 2.4
Environment: 
 System:          
 Architecture: 

Description: 
  ----------
  X-Sun-Data-Type: text
  X-Sun-Data-Description: text
  X-Sun-Data-Name: text
  X-Sun-Charset: us-ascii
  X-Sun-Content-Lines: 3
  
  (apply-extensionality) bombs PVS with a
  "No methods applicable for generic function" error message when applied
  to function override expressions. The details are contained in the .dmp file.
  ----------
  X-Sun-Data-Type: default
  X-Sun-Data-Description: default
  X-Sun-Data-Name: bug_apply_ext_WITH.dmp
  X-Sun-Charset: us-ascii
  X-Sun-Content-Lines: 71
  
  
  $$$bug_apply_ext_WITH.pvs
  %==========================================
  % PVS 2.4 bug: (APPLY-EXTENSIONALITY) bombs
  % on a function override expression
  %
  % Ralph D. Jeffords
  % 11 dec. 2001
  %==========================================
  bug_apply_ext_WITH:THEORY
  BEGIN
  
  ID: TYPE = { X, Y }
  
  State: TYPE = [ r:ID -> nat ]
  
  	s: VAR State
  
  %-----------------------------------------------------------------
  % (APPLY-EXTENSIONALITY) bombs with this message:
  %
  %Error: No methods applicable for generic function
  %       #<STANDARD-GENERIC-FUNCTION DOMAIN> with args (number) of
  %       classes (TYPE-NAME)
  %  [condition type: PROGRAM-ERROR]
  %-----------------------------------------------------------------
  
   
  bombing_proof: THEOREM
  
  	s WITH [ (X) := 0, (Y) := 0 ] = s WITH [ (Y) := 0, (X) := 0 ]
  
  %-----------------------------------------------------------------
  % WORKAROUND: use (NAME) to name the override expressions, replace
  % the override expressions with these names, then everything
  % works okay
  %-----------------------------------------------------------------
  
  
  ok_proof: THEOREM
  
  	s WITH [ (X) := 0, (Y) := 0 ] = s WITH [ (Y) := 0, (X) := 0 ]
  
  	
  
  END bug_apply_ext_WITH
  
  $$$bug_apply_ext_WITH.prf
  (|bug_apply_ext_WITH|
   (|bombing_proof| "" (SKOSIMP) (("" (APPLY-EXTENSIONALITY) NIL)))
   (|ok_proof| "" (SKOSIMP)
    (("" (NAME "s1" "s!1 WITH [(X) := 0, (Y) := 0]")
      (("" (NAME "s2" "s!1 WITH [(Y) := 0, (X) := 0]")
        (("" (REPLACE -1)
          (("" (REPLACE -2)
            (("" (APPLY-EXTENSIONALITY :HIDE? T)
              (("" (REPLACE -1 + RL)
                (("" (REPLACE -2 + RL)
                  (("" (HIDE -1 -2)
                    (("" (LIFT-IF)
                      (("" (LIFT-IF) (("" (PROPAX) NIL NIL)) NIL)) NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  

How-To-Repeat: 

Fix: 
Fixed check-for-tccs* (update-expr funtype) to recurse down the
assignments correctly.

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