[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: pvs-help@csl.sri.com*Subject*: Re: proving a property over finite_sets*From*: Jerry James <james@ittc.ku.edu>*Date*: Mon, 18 Aug 2003 11:50:11 -0500*Cc*: Borzoo Bonakdarpour <borzoo@cse.msu.edu>*References*: <Pine.GSO.4.31.0308111551520.4212-100000@ftl.cse.msu.edu>*Reply-To*: Jerry James <james@ittc.ku.edu>*Sender*: pvs-help-owner@csl.sri.com*User-Agent*: Gnus/5.1002 (Gnus v5.10.2) XEmacs/21.4 (Rational FORTRAN, linux)

Borzoo Bonakdarpour <borzoo@cse.msu.edu> wrote: > I have been struggling to prove an easy-looking property of the following > specification: > > state: TYPE > f: finite_set[[state, state]] > > s0, s1: VAR state > X: finite_set[state] > > set1(rs: finite_set[state]): finite_set[state] = > {s0 | EXISTS (s1): (member(s1, rs) AND member((s0, s1), f))} > > func (fpSet: finite_set[state]) : RECURSIVE finite_set[state] = > LET rs = set1(fpSet) IN > IF nonempty?(rs) THEN > func (union(rs, fpSet)) > ELSE > fpSet > ENDIF > > MEASURE card(complement(fpSet)) > > prop: LEMMA FORALL(s0, s1): (member((s0, s1), f) AND member(s1, > func(X))) IMPLIES member(s0, func(X)) > > I tried induction schemes on finite_Sets and mucalculs without any > success. I appreciate if your share your thoughts on how to prove this > with me. Your specification has a couple of problems. First, the measure for your recursive function is over "complement(fpSet)". But since the type "state" is not known to be finite, "complement(fpSet)" may be infinite, making the "card" function inapplicable. If you meant the state type to be finite, you'll have to say so; if not, then you need to rethink the definition of "func". Second, you cannot prove the termination property of "func" as stated. Here is a counterexample: state = { s0, s1 } f = { (s0, s1), (s1, s0) } Now func({s0, s1}) will never terminate, since rs is nonempty each time, but rs = union(rs, fpSet). If you mean for f to be a function, then you'll have to say that. Or perhaps you meant for the conditional to be "IF nonempty?(difference(rs, fpSet))" instead? Once you get those problems cleared up, I'll bet that you'll find it easier to prove the result you want. I'd start with an easier lemma, something along these lines: func_monotonic: LEMMA FORALL (A: finite_set[state]), s0: member(s0, A) IMPLIES member(s0, func(A)) As for induction, how does your paper proof look? What is it that you are inducting over? Regards, -- Jerry James Assistant Professor EECS Department University of Kansas

- Prev by Date:
**proving a property over finite_sets** - Next by Date:
**Re: proving a property over finite_sets** - Prev by thread:
**proving a property over finite_sets** - Next by thread:
**Re: proving a property over finite_sets** - Index(es):