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