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

*To*: Borzoo Bonakdarpour <borzoo@cse.msu.edu>*Subject*: Re: problem with finite types*From*: Bruno Dutertre <bruno@sdl.sri.com>*Date*: Tue, 11 Mar 2003 18:50:39 -0800*CC*: pvs-help@csl.sri.com*References*: <Pine.GSO.4.31.0303101934580.18653-100000@arctic.cse.msu.edu>*Sender*: pvs-help-owner@csl.sri.com*User-Agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.0.0) Gecko/20020529

Borzoo Bonakdarpour wrote: > Hi, > > I am writing a specification to calculate the finite set of states, which > have a path to a particular state. The spec looks like: > > reachable[state : TYPE]: THEORY > > BEGIN > > ASSUMING > > IMPORTING state[state] > > SP_is_finite : ASSUMPTION is_finite_type[StatePred] > AC_is_finite : ASSUMPTION is_finite_type[Action] > > ENDASSUMING > > s0, s1 : VAR state > > reverse_reachable_states(x : StatePred, f : Action) : StatePred = > (LAMBDA s0 : member(s0, x) AND (EXISTS (s1 : state) : member((s0, s1), f) AND member(s1, x))) > > fpcal (ms: StatePred, f: Action) : RECURSIVE StatePred = > > IF nonempty?(reverse_reachable_states(ms, f)) THEN > fpcal (union(reverse_reachable_states(ms, f), ms), f) > ELSE ms > ENDIF > > MEASURE card(ms) > > END reachable > > where StatePred : TYPE = PRED[state] and Action : TYPE = PRED[[state, state]] > > I got a TCC: > > % Subtype TCC generated (at line 26, column 15) for ms > % expected type S: finite_set[state] > % unfinished > fpcal_TCC1: OBLIGATION FORALL (ms: StatePred[state]): > is_finite[state](ms); > > and I have reached this point in proof: > > {-1} is_finite_type[StatePred] > |------- > [1] is_finite[state](ms!1) > > which looks very simple, but seems there is no way to prove it. There > must be something wrong somewhere else. Does anybody have any idea? > > Thanks, > Borzoo > Hi, The assumption is_finite_type[StatePred] specifies that there are only finitely many functions of type PRED[state]. That's sufficient to prove that ms!1 is finite, but in an indirect way. What you probably need to assume is that there are finitely many states, that is, "is_finite_type[state]". Bruno -- Bruno Dutertre | bruno@sdl.sri.com SDL, SRI International | fax: 650 859-2844 333 Ravenswood Avenue, Menlo Park CA 94025 | tel: 650 859-2717

- Prev by Date:
**problem with finite types** - Next by Date:
**rewrite rule for expressions inside LAMBDA** - Prev by thread:
**problem with finite types** - Next by thread:
**Induction derivation tree** - Index(es):