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

*To*: pvs-help@csl.sri.com*Subject*: [PVS-Help] Deferring TCCs*From*: robert <robert@itee.uq.edu.au>*Date*: Wed, 05 Jan 2005 20:09:20 +1000*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>*Sender*: pvs-help-bounces+archive=csl.sri.com@csl.sri.com

Hi, is there a way of deferring TCCs generated from definitions to being checked where the definitions are used in a theorem? For instance, consider the following theory: first_one: THEORY BEGIN l: VAR list[nat] first_one(l): bool = car(l) = 1 END first_one It generates one TCC: first_one_TCC1: OBLIGATION FORALL (l: list[nat]): cons?[nat](l); This can apparently never be satisfied, ie, every proof that depends on first_one will only ever be "proved - incomplete". However I can be careful with my use of first_one such that any time it is used in a theorem its actual parameter will satisfy the TCC (ie. is non-null). (In fact, it seems to me that I would not be able to prove anything useful using first_one if the parameter is nonempty since 'car' is meaningless in this case.) Is there a general workaround that scales for many theorems like first_one with possibly non-trivial TCCs? One option is to add "cons?(l) and" to the definition, but this is redundant if I know first_one will only be used in a context where cons?(l) is satisfied, and in general the approach can clutter the definitions if the conditions required to avoid generating TCCs are nontrivial. Perhaps there is another way of dealing with the situation, along the lines of using judgements. What I'd like to see is first_one generate a TCC 'flag', as above. Then consider a theorem which uses first_one, eg, th: THEORY BEGIN importing first_one l: VAR list[nat] x: THEOREM (forall l: l = (: 1 :) implies first_one(l)) END th The theorem generates the TCC (forall l: l = (: 1 :) implies cons?(l)) Can this sort of behaviour be achieved in PVS? Or is there some reason why it is a bad idea? Rob

- Prev by Date:
**[PVS-Help] Decompose-equality after assert** - Next by Date:
**Re: [PVS-Help] Deferring TCCs** - Prev by thread:
**[PVS-Help] Proof: limit of strictly monotonic function over naturals** - Next by thread:
**Re: [PVS-Help] Deferring TCCs** - Index(es):