[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] Deferring TCCs
PVS sub-typing mechanism is intended for this kind of situations. You
l: VAR (cons?[nat])
first_one(l): bool = car(l) = 1
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
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?
Cesar A. Munoz H., Senior Staff Scientist mailto:email@example.com
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