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

PVS Bug 392

Synopsis:        Coercion changes meaning
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Thu Nov 11 01:57:27 1999
Originator:      Chris George
Organization:    iist.unu.edu
Release:         PVS 2.3

  This is a multi-part message in MIME format.
  Content-Type: text/plain; charset=us-ascii
  Content-Transfer-Encoding: 7bit
  There are two related bugs exhibited by the attached file bug.pvs.
  1.  The lemma bug is proved by the proof (SKOSIMP*) (AUTO-REWRITE-DEFS
  T) (ASSERT), but it is not valid.  The same proof applied to the lemma
  OK fails as it should.
  The only difference in the two lemmas is the coercion.
  This happens with pvs versions 2.2 and 2.3 (using Debian Linux in case
  this is significant).
  The coercion applied seems to be coercing s from set of Element to set
  of (type1?), and this is not valid.  The coercion of the single element
  from (type1?) to Element, forced in the lemma OK, is valid.
  2.  If bug.pvs is pretty printed some additional functions appear
  (presumably making coercions explicit).  The result will not type
  check.  I would expect pretty-printing to be neutral.  (In fact I am
  surprised that it changes anything other than white space.)  Again
  versions 2.2 and 2.3 behave the same.
  I now have a fairly substantial proof, involving expressions like that
  in the lemma bug, that I can no longer rely on.  Help!
  Chris George
  Content-Type: text/plain; charset=us-ascii;
  Content-Transfer-Encoding: 7bit
  Content-Disposition: inline;
  bug: THEORY
    Element: DATATYPE
      type1(num1 : nat): type1?
      type2(num2 : nat): type2?
    END Element
    Set : TYPE = setof[Element]
    s : VAR Set
    n : VAR nat
    isin(n, s): bool =
      member(type1(n), s) OR member(type2(n),s)
    bug: LEMMA
      NOT isin(n,difference(s, singleton(type1(n))))
      NOT isin(n,difference(s, singleton(type1(n):Element)))
   END bug


 [dave_sc, 4/16/01]
 1) The typechecker is inserting an extend and restrict into the expression
    which are not needed and create an expression with different semantics
    than the intended one.
 2) This is likely M-x ppe, which is not intended to produce a typecheckable
    buffer (hence M-x tc won't run on a .ppe buffer).  M-x ppf produces output
    that is typecheckable (confirmed on this example).

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