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

*To*: robert <robert@itee.uq.edu.au>*Subject*: Re: [PVS-Help] Deferring TCCs*From*: "Cesar A. Munoz" <munoz@nianet.org>*Date*: Wed, 05 Jan 2005 09:59:35 -0500*Cc*: pvs-help@csl.sri.com*In-Reply-To*: <200501051009.j05A9tXp009455@mx1.csl.sri.com>*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>*Organization*: NIA*References*: <200501051009.j05A9tXp009455@mx1.csl.sri.com>*Sender*: pvs-help-bounces+archive=csl.sri.com@csl.sri.com

Bob, PVS sub-typing mechanism is intended for this kind of situations. You can declare: first_one: THEORY BEGIN l: VAR (cons?[nat]) first_one(l): bool = car(l) = 1 END first_one cons? is the subtype of lists with at least one element. No TCCS are generated during the type-checking of the theory. TCCs will be generated for actual arguments of first_one and in most cases they will be automatically discharged. Cesar On Wed, 2005-01-05 at 05:09, robert wrote: > 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 -- Cesar A. Munoz H., Senior Staff Scientist mailto:munoz@nianet.org National Institute of Aerospace mailto://C.A.Munoz@larc.nasa.gov 144 Research Drive http://research.nianet.org/~munoz Hampton, VA 23666, USA Tel. +1 (757) 766 1539 Fax +1 (757) 766 1855

- Prev by Date:
**[PVS-Help] Deferring TCCs** - Next by Date:
**Re: [PVS-Help] pvs-strategies** - Prev by thread:
**[PVS-Help] Deferring TCCs** - Next by thread:
**Re: [PVS-Help] Deferring TCCs** - Index(es):