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

PVS Bug 493


Synopsis:        rewrite/importing bug (PVS 2.3 with patches)
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Thu Nov  2 18:40:02 2000
Originator:      Paul Y Gloess
Organization:    labri.u-bordeaux.fr
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  This is a multi-part message in MIME format.
  --------------D2AE7DBF5B63D9B228873C23
  Content-Type: text/plain; charset=us-ascii
  Content-Transfer-Encoding: 7bit
  
  Dear PVS hackers:
  
  We found a bug with rewrite in a very specific circumstance.
  
  In short: in the course of the proof of a lemma, a REWRITE command works
  fine, but if we add a very simple recursive definition right after the
  lemma, the REWRITE command no longer works, although it still finds the
  adequate substitution.
  
  I tried to minimize the bug as much as possible: it seems to be related
  with an abstract datatype (using "WITH SUBTYPES"). Note that the bug no
  longer occurs if the recursive definition (of "record_patterns") is
  replaced with a non recursive equivalent one (that always returns
  "emptyset").
  
  The attached (very short) dump is self explanatory.
  
  Best regards,
  
  --
  Paul Y Gloess
            LaBRI:   http://dept-info.labri.u-bordeaux.fr/~gloess
     E.N.S.E.R.B.:   http://www.enserb.fr/~gloess
  
  
  
  --------------D2AE7DBF5B63D9B228873C23
  Content-Type: text/plain; charset=us-ascii;
   name="bug.importing.2_november_2000.rewrite_inhibited.dump"
  Content-Transfer-Encoding: 7bit
  Content-Disposition: inline;
   filename="bug.importing.2_november_2000.rewrite_inhibited.dump"
  
  %Patch files loaded: patch2 version 1.2.2.36
  
  $$$rewrite_inhibited.pvs
  %%%
  %%% Paul Y Gloess <Paul.Gloess@LaBRI.U-Bordeaux.Fr>
  %%%   http://dept-info.labri.u-bordeaux.fr/~gloess/
  %%%   http://www.enserb.fr/~gloess/
  %%%
  %%% Bug report, 2 november 2000, with PVS 2.3 (and above patches):
  %%%
  %%%   A REWRITE proof command, in the course of the proof of lemma,
  %%%    does not work when some recursive definition follows the
  %%%    lemma in the theory; the same REWRITE command works fine
  %%%    when the recursive definition is commented out.
  %%%    
  %%%   To reproduce bug, try the proof of "rewrite_subset_member"
  %%%    lemma below; after the COMMENT command, try (REWRITE "subset_member")
  %%%    and observe that it fails although PVS finds a correct substitution.
  %%%    Restart the proof after commenting out the "record_patterns" definitio
 n,
  %%%    and notice that (REWRITE "subset_member") works fine.
  %%%
  rewrite_inhibited[str: TYPE]: THEORY
  
    BEGIN
  
      IMPORTING adt[str]
  
      IMPORTING list_to_set[elementType[str]]
  
      rewrite_subset_member: LEMMA
        (FORALL (ets: setof[elementType[str]], etl: list[elementType[str]]):
           subset?(ets, set(etl))
             =
           (FORALL (et: (ets)): member(et, etl))) ;
  
      record_patterns(etl: list[elementType[str]])
        : RECURSIVE setof[str]
        = CASES etl OF
            null: emptyset,
            cons(et, etlr): record_patterns(etlr)
          ENDCASES
        MEASURE identity
        BY << ;
  
    END rewrite_inhibited
  
  
  $$$rewrite_inhibited.prf
  (|rewrite_inhibited|
   (|rewrite_subset_member| "" (SKOLEM * ("ets" "etl"))
    ((""
      (COMMENT "When record_patterns definition is present in this theory,
  the (rewrite \"subset_member\") proof command does not work here,
  although PVS finds the correct substitution for ts and tl variables;
  when the definition is commented out, this rewrite command works.")
      (("" (REWRITE "subset_member") NIL
        ";;;When record_patterns definition is present in this theory,
  ;;;the (rewrite \"subset_member\") proof command does not work here,
  ;;;although PVS finds the correct substitution for ts and tl variables;
  ;;;when the definition is commented out, this rewrite command works."))
      NIL))
    NIL)
   (|record_patterns_TCC1| "" (WELL-FOUNDED-TCC))
   (|record_patterns_TCC2| "" (TERMINATION-TCC) NIL NIL))
  
  
  $$$list_to_set.pvs
  list_to_set[T: TYPE]: THEORY
  
    BEGIN
  
      set(l: list[T]): setof[T]
        = {t: T | member(t, l)} ;
  
      subset_member: LEMMA
        (FORALL (ts: setof[T], tl: list[T]):
           subset?(ts, set(tl))
             =
           (FORALL (t: (ts)): member(t, tl))) ;
  
    END list_to_set
  
  $$$list_to_set.prf
  (|list_to_set|
   (|subset_member| "" (SKOLEM * ("ts" "tl"))
    (("" (IFF)
      (("" (GROUND)
        (("1" (SKOLEM * "t")
          (("1" (TYPEPRED "t")
            (("1" (EXPAND "subset?")
              (("1" (INST?)
                (("1" (EXPAND "member" :IF-SIMPLIFIES T)
                  (("1" (EXPAND "set") (("1" (PROPAX) NIL NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL)
         ("2" (EXPAND "subset?")
          (("2" (SKOLEM * "t")
            (("2" (EXPAND "member" :IF-SIMPLIFIES T)
              (("2" (FLATTEN)
                (("2" (EXPAND "set") (("2" (INST?) NIL NIL)) NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|subset_member2| "" (SKOLEM * ("ts" "tl" "t"))
    (("" (TYPEPRED "t")
      (("" (FLATTEN)
        (("" (REWRITE "subset_member") (("" (INST?) NIL NIL)) NIL)) NIL))
      NIL))
    NIL))
  
  
  $$$adt.pvs
  adt[str: TYPE]: THEORY
  
    BEGIN
  
      adt: DATATYPE WITH SUBTYPES elementType
  
      BEGIN
  
        ElementType(ET: str): ElementType?: elementType
  
      END adt
  
    END adt
  
  
  --------------D2AE7DBF5B63D9B228873C23--

How-To-Repeat: 

Fix: 

 [davesc]
 Fixed in 2.3.1

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