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

Re: [PVS-Help] Deferring TCCs



Thanks Cesar, 

Putting subtypes everywhere was again something I was hoping to
avoid.  It adds clutter, and is another thing that must be changed
as the specification is changed.  However I guess that's the price
you have to pay for rigor.. (I've followed your advice and have
patched my specification with subtypes appropriately.)

Is there a particular reason why type checks must be made on a
declaration, rather than where the decl. is used in a theorem?
Static type checking as in PVS is obviously desirable, but, as in
this case, gets in the way of some proofs.  Maybe one of the papers
discusses how PVS TCCs contribute to correctness?

Thanks,
Rob

On Wed, 5 Jan, "Cesar A. Munoz" wrote:
: 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