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

*To*: pvs-help@xxxxxxxxxxx*Subject*: Re: [PVS-Help] Expected type TCC*From*: Jerome <jerome@xxxxxxxxxxxxxx>*Date*: Sat, 26 Apr 2008 22:55:20 -0700*In-reply-to*: <20080423002424.GB7342@cs.caltech.edu>*List-help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-id*: PVS-Help <pvs-help.csl.sri.com>*List-post*: <mailto:pvs-help@csl.sri.com>*List-subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*References*: <20080423002424.GB7342@cs.caltech.edu>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx*User-agent*: Mutt/1.4.1i

I have a similar recursive definition presented in my earlier email: >example: THEORY BEGIN > index: TYPE = posnat > value: TYPE = real > indices: TYPE = non_empty_finite_set[index] > myset: TYPE = [index -> value] > fun: TYPE = FUNCTION[value, value -> value] > > curry(f: fun, m: myset, I: indices): RECURSIVE value = > LET i: index = choose(I) IN > IF singleton?(I) THEN m(i) > ELSE f(m(i), curry(f, m, remove(i, I))) > ENDIF > MEASURE card(I) >END example My question, again, is in regards to the TCC's generated. In my last email, I asked about TCC2; this time I could use some help with TCC1: curry_TCC1: OBLIGATION FORALL (I: indices, i: index): NOT singleton?(I) AND i = choose(I) IMPLIES NOT empty?[index](remove[index](i, I)); Using finite_sets_sum as an example (as Jerry had mentioned), a similar TCC is discharge using '(SUBTYPE-TCC)'. Unfortunately, applying the same rule to my curry_TCC1 isn't as successful. What exactly does SUBTYPE-TCC do (that it's so successful in the finite_sets_sum case)? Is there a similar method I can use in my case? Thanks again. jerome

- Prev by Date:
**Re: [PVS-Help] Termination TCC** - Next by Date:
**Re: [PVS-Help] Expected type TCC** - Prev by thread:
**Re: [PVS-Help] The problem with self-stability example** - Next by thread:
**Re: [PVS-Help] Expected type TCC** - Index(es):