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