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

PVS Bug 624


Synopsis:        False type predicate
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Tue Dec  3 15:45:04 2001
Originator:      Jerry James
Organization:    eecs.ku.edu
Release:         PVS 2.4
Environment: 
 System:          
 Architecture: 

Description: 
  --=-=-=
  
  The attached dump file contains a stripped down version of a theory I
  use locally to get function inverses without having to show nonemptiness
  of the range type.  Upon introducing a particular JUDGEMENT into this
  file, I noticed that a TYPEPRED used in some of the proofs would
  introduce a predicate that was not necessarily true.  The comments in
  the file show where the bug occurs, and how to use it to prove false
  results.
  
  Regards,
  -- 
  Jerry James
  Assistant Professor
  EECS Department
  University of Kansas
  
  
  
  --=-=-=
  Content-Type: application/octet-stream
  Content-Disposition: attachment; filename=pvs_bug.dmp
  Content-Description: Dump file demonstrating bug
  
  
  $$$judgement_bug.pvs
  judgement_bug[D: TYPE, R: TYPE]: THEORY
   BEGIN
  
    d: VAR D
    r: VAR R
    f: VAR [D -> R]
    g: VAR [R -> D]
  
    IMPORTING functions[D, R]
  
    inverse?(f)(g): bool = FORALL r: (EXISTS d: f(d) = r) => f(g(r)) = r
    invertible?(f): bool = EXISTS g: inverse?(f)(g)
  
    % =========================================================================
 =
    % Invertible functions
    %
    % A function is invertible based on the theory parameter types, not any
    % feature of the function itself.  However, the existence of certain types
    % of functions tells us all we need to know about the types.
    % =========================================================================
 =
    invertible_type: LEMMA
      FORALL f: invertible?(f) IFF (EXISTS d: TRUE) OR (FORALL r: FALSE)
  
    surjective_is_invertible: JUDGEMENT
      (surjective?[D, R]) SUBTYPE_OF (invertible?)
  
    inverse_alt(f: (invertible?)): (inverse?(f)) = choose({g | inverse?(f)(g)})
  
    bijective_inverse_is_bijective: JUDGEMENT
      inverse_alt(f: (bijective?[D,R])) HAS_TYPE (bijective?[R,D])
  
    % This is false, but PVS lets me prove it.  The TYPEPRED step is the
    % culprit.  It introduces a true "inverse?" predicate, and a bogus
    % "bijective?" predicate
    inverse_is_bijective: LEMMA
      FORALL (f: (invertible?)): bijective?(inverse_alt(f))
  
   END judgement_bug
  
  
  % With the false inverse_is_bijective in hand, we can prove obviously false
  % results
  judgement_bug_below: THEORY
   BEGIN
  
    IMPORTING judgement_bug[below[1], below[2]]
  
    below1_below2_bijective: THEOREM
      EXISTS (f: [below[2] -> below[1]]): bijective?(f)
  
   END judgement_bug_below
  
  $$$judgement_bug.prf
  (|judgement_bug|
   (|invertible_type| (:NEW-GROUND? T) "" (SKOLEM!)
    (("" (EXPAND "invertible?")
      (("" (PROP)
        (("1" (SKOSIMP*) (("1" (INST + "g!1(r!1)") NIL NIL)) NIL)
         ("2" (INST + "LAMBDA r: (epsilon! d: f!1(d) = r)")
          (("1" (EXPAND "inverse?")
            (("1" (SKOSIMP*)
              (("1" (USE "epsilon_ax[D]")
                (("1" (ASSERT) (("1" (INST?) NIL NIL)) NIL)
                 ("2" (INST?) NIL NIL))
                NIL))
              NIL))
            NIL)
           ("2" (SKOLEM!) NIL NIL))
          NIL)
         ("3" (LEMMA "fun_exists[R, D]")
          (("3" (PROP)
            (("1" (SKOLEM!)
              (("1" (INST + "f!2")
                (("1" (EXPAND "inverse?")
                  (("1" (SKOSIMP*) (("1" (INST?) NIL NIL)) NIL)) NIL))
                NIL))
              NIL)
             ("2" (SKOLEM!) (("2" (INST - "x!1") NIL NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|surjective_is_invertible| (:NEW-GROUND? T) "" (SKOLEM-TYPEPRED)
    (("" (REWRITE "invertible_type")
      (("" (FLATTEN)
        (("" (EXPAND "surjective?")
          (("" (SKOLEM!)
            (("" (INST - "r!1") (("" (SKOLEM!) (("" (INST?) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|inverse_alt_TCC1| (:NEW-GROUND? T) "" (SUBTYPE-TCC) NIL NIL)
   (|bijective_inverse_is_bijective| (:NEW-GROUND? T) "" (SKOLEM-TYPEPRED)
    (("" (TYPEPRED "inverse_alt(f!1)")
      (("" (EXPAND* "inverse?" "bijective?" "injective?" "surjective?")
        (("" (PROP)
          (("1" (SKOSIMP)
            (("1" (INST-CP - "x2!1")
              (("1" (INST - "x1!1")
                (("1" (SPLIT)
                  (("1" (SPLIT)
                    (("1" (ASSERT) NIL NIL) ("2" (INST -4 "x2!1") NIL NIL)) NIL
 )
                   ("2" (INST -4 "x1!1") NIL NIL))
                  NIL))
                NIL))
              NIL))
            NIL)
           ("2" (SKOLEM!)
            (("2" (INST + "f!1(y!1)")
              (("2" (INST - "f!1(y!1)")
                (("2" (SPLIT)
                  (("1" (INST - "inverse_alt(f!1)(f!1(y!1))" "y!1")
                    (("1" (ASSERT) NIL NIL)) NIL)
                   ("2" (INST + "y!1") NIL NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|inverse_is_bijective| (:NEW-GROUND? T) "" (SKOLEM-TYPEPRED)
    (("" (TYPEPRED "inverse_alt(f!1)") (("" (PROPAX) NIL NIL)) NIL)) NIL))
  (|judgement_bug_below|
   (|below1_below2_bijective| (:NEW-GROUND? T) ""
    (INST + "inverse_alt(LAMBDA (x: below[1]): x)")
    (("1" (LEMMA "inverse_is_bijective")
      (("1" (INST - "LAMBDA (x: below[1]): x")
        (("1" (EXPAND "invertible?")
          (("1" (INST + "LAMBDA (y: below[2]): 0")
            (("1" (EXPAND "inverse?")
              (("1" (SKOSIMP :PREDS? T) (("1" (ASSERT) NIL NIL)) NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL)
     ("2" (EXPAND "invertible?")
      (("2" (INST + "LAMBDA (y: below[2]): 0")
        (("2" (EXPAND "inverse?")
          (("2" (SKOSIMP :PREDS? T) (("2" (ASSERT) NIL NIL)) NIL)) NIL))
        NIL))
      NIL))
    NIL))
  
  
  --=-=-=--
  

How-To-Repeat: 

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