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

PVS Bug 620


Synopsis:        distilled problem
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Tue Nov 27 13:56:34 2001
Originator:      John Rushby
Organization:    csl.sri.com
Release:         PVS 2.4
Environment: 
 System:          
 Architecture: 

Description: 
  Here's the problem with linkfaults distilled to a mimimum.  The
  problem is the proof of count_status.  It works in PVS 2.3 but fails
  in 2.4.  It doesn't work because the (rewrite "card_u") step doesn't
  find a match.  I'm unable to understand whether the problem is in the
  change in associativity, automatic simplifications being done that
  weren't done before, or failure of higher-level matching.
  
  Elsewhere, I used to use auto rewriting of norm_assocr to mormalize
  associativity, but that started looping in PVS 2.4.  In this
  particular proof, it has no effect, but might be a symptom of similar
  problems.
  
  John
  
  
  $$$pvs-strategies
  (defstep subtype-tcc ()
    (grind :rewrites ("finite_below") :defs explicit)
  "Modified subtyp-tcc rule to use finite_below"
  "By modified TCC strategy"
  )
  
  
  $$$bug.pvs
  xcardprops[T: NONEMPTY_TYPE]: THEORY
  BEGIN
  
    A,B,C,D: VAR finite_set[T]
  
    IMPORTING finite_sets@finite_sets_below,
    finite_sets@finite_sets_pred
  
    r,s,t: VAR bool
  
    norm_assocl: SUBLEMMA (r AND (s AND t)) = ((r AND s) AND t)
    norm_assocr: SUBLEMMA ((r AND s) AND t) = (r AND (s AND t))
    norm_assoclo: SUBLEMMA (r OR (s OR t)) = ((r OR s) OR t)
    norm_assocro: SUBLEMMA ((r OR s) OR t) = (r OR (s OR t))
  
    equal_card: SUBLEMMA A=B => card(A)=card(B)
  
  END xcardprops
  
  bug[n: posnat, T: NONEMPTY_TYPE]: THEORY
  BEGIN
    
    npos: LEMMA n > 0
    node: TYPE+ = below[n] CONTAINING 0
    
    IMPORTING xcardprops[node],
      finite_sets@finite_sets_below,
      finite_sets@finite_sets_pred
  
    nodeset: TYPE = finite_set[node]
  
    p,q: VAR node
  
    A,B,C,D,Z,W: var nodeset
  
    faults: TYPE = {good, manifest, omission, symmetric, arbitrary}
  
    status(p): faults
    
    ok(p): bool = good?(status(p))
    man(p): bool = manifest?(status(p))
    omit(p): bool = omission?(status(p))
    sym(p): bool = symmetric?(status(p))
    arb(p): bool = arbitrary?(status(p))
  
    card_u: SUBLEMMA disjoint?(Z,W) IMPLIES
      card({q|A(q) AND (Z(q) or W(q))}) = card({q|A(q) AND
      Z(q)})+card({q|A(q) AND W(q)})
  
    count_status: LEMMA card(A) = 
      card({q|A(q) AND man(q)})
       + card({q|A(q) AND ok(q)})
       + card({q|A(q) AND omit(q)})
       + card({q|A(q) AND arb(q)})
       + card({q|A(q) AND sym(q)})
  
  end bug
  
  $$$bug.prf
  (|xcardprops| (|equal_card| "" (GRIND) NIL NIL))
  (|bug| (|node_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|card_u_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|card_u_TCC2| "" (SUBTYPE-TCC) NIL NIL)
   (|card_u_TCC3| "" (SUBTYPE-TCC) NIL NIL)
   (|card_u| "" (AUTO-REWRITE "finite_below")
    (("" (SKOSIMP)
      ((""
        (CASE-REPLACE "card({q | A!1(q) AND (Z!1(q) OR W!1(q))}) =
                   card(union({q | A!1(q) AND Z!1(q)},{q | A!1(q) AND W!1(q)}))
 "
         :HIDE? T)
        (("1" (REWRITE "card_union")
          (("1" (ASSERT)
            (("1"
              (CASE "empty?(intersection({q | A!1(q) AND Z!1(q)}, {q | A!1(q) A
 ND W!1(q)}))")
              (("1" (REWRITE "empty_card") NIL NIL)
               ("2" (HIDE 2) (("2" (GRIND) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL)
         ("2" (HIDE 2)
          (("2" (REWRITE "equal_card[node]")
            (("2" (HIDE 2)
              (("2" (APPLY-EXTENSIONALITY :HIDE? T)
                (("2" (GRIND) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|count_status_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|count_status_TCC2| "" (SUBTYPE-TCC) NIL NIL)
   (|count_status_TCC3| "" (SUBTYPE-TCC) NIL NIL)
   (|count_status_TCC4| "" (SUBTYPE-TCC) NIL NIL)
   (|count_status_TCC5| "" (SUBTYPE-TCC) NIL NIL)
   (|count_status| "" (SKOSIMP)
    (("" (AUTO-REWRITE "finite_below")
      ((""
        (CASE-REPLACE
         "card(A!1)=card({q | A!1(q) AND ( man(q) or omit(q) or arb(q) or ok(q)
  or sym(q))})")
        (("1" (HIDE -1)
          (("1" (REWRITE "card_u")
            (("1" (REWRITE "card_u")
              (("1" (REWRITE "card_u")
                (("1" (REWRITE "card_u")
                  (("1" (ASSERT) NIL)
                   ("2" (HIDE 2) (("2" (GRIND) NIL)))))
                 ("2" (HIDE 2) (("2" (GRIND) NIL)))))
               ("2" (HIDE 2) (("2" (GRIND) NIL)))))
             ("2" (HIDE 2) (("2" (GRIND) NIL)))))))
         ("2" (HIDE 2)
          (("2" (REWRITE "equal_card[node]")
            (("2" (APPLY-EXTENSIONALITY :HIDE? T)
              (("2" (GRIND) NIL))))))))))))))
  

How-To-Repeat: 

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