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

*To*: Jerry James <james@ittc.ku.edu>*Subject*: Re: proving a property over finite_sets*From*: Borzoo Bonakdarpour <borzoo@cse.msu.edu>*Date*: Sat, 23 Aug 2003 12:05:01 -0400 (EDT)*cc*: <pvs-help@csl.sri.com>*In-Reply-To*: <psisousyf0.fsf@diannao.ittc.ku.edu>*Sender*: pvs-help-owner@csl.sri.com

Hi, Thanks for your reply. Actually I didn't have the mentioned problems in my original specification (such as defining "state" as a finite type and ...). The main problem was using finite_sets induction schemes. I modified my finite_set based recursive function to another function which is based on the number of steps that makes the final set and I proved all my lemmas and theorem :) It is much easier to deal with induction on integers rather than finite-sets. Here is what I did: func(i: nat): RECURSIVE finite_set[state] = IF i = 0 THEN init ELSE union(func(i-1), set1(func(i-1))) ENDIF MEASURE (LAMBDA (x: nat): x) I was also able to prove that this definition is equal to the previous using a couple of intermediate lemmas. Thanks, Borzoo On Mon, 18 Aug 2003, Jerry James wrote: > 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 >

**References**:**Re: proving a property over finite_sets***From:*Jerry James <james@ittc.ku.edu>

- Prev by Date:
**Re: proving a property over finite_sets** - Next by Date:
**[pvs startup] Unable to locate enough free space...** - Prev by thread:
**Re: proving a property over finite_sets** - Next by thread:
**"assertion itheory failed" error** - Index(es):