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
Environment: 
 System:          
 Architecture: 

Description: 
  This is a multi-part message in MIME format.
  --------------1871DE380E9508DAB65D8212
  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!
  
  Regards,
  
  Chris George
  --------------1871DE380E9508DAB65D8212
  Content-Type: text/plain; charset=us-ascii;
   name="bug.pvs"
  Content-Transfer-Encoding: 7bit
  Content-Disposition: inline;
   filename="bug.pvs"
  
  bug: THEORY
   BEGIN
  
    Element: DATATYPE
    BEGIN
      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))))
  
    OK: LEMMA
      NOT isin(n,difference(s, singleton(type1(n):Element)))
  
   END bug
  
  
  --------------1871DE380E9508DAB65D8212--

How-To-Repeat: 

 [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).

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