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

*To*: pvs-help@csl.sri.com*Subject*: 2 Questions*From*: Bettina Buth <bb@Informatik.Uni-Bremen.DE>*Date*: Wed, 11 Jun 1997 15:04:52 +0200

Hello, I'm working with PVS as a backend to a proof obligation generator and going through a case study right now. There are two questions which I would like to place here: 1. I encounter problems with the TCCs generated for my obligations: due to the automatic process of generation I do not have any influence concerning the order of subcomponents of a formula. Since PVS only considers those subcomponents that preceed the one that induces the TCC are used as permise for the proof I have TCCs which I can't prove since the relevant information is standing after that. E.g. ( A AND P(front(x)) AND NOT (empty?(x)) ) where x is an element of a list type supposes me to prove A => not (empty? (x)) which I usually can't do without the additional information. Has anyone encountered similar problems? Has anyone found a solution? Sam, did you consider any options for this? 2. A more basic technical problem: I would like to replace a single occurrence of a term in a formula that contains multiple occurrences of the term. I couldn't find a way of using expand, rewrite or replace for this. More concrete: I have a lemma l = r and a formula f (g(l), h(l)) and I would like to replace only the occurrence of l in "g(l)" with r. Is there a possibility to do this? As far as I found rewrite and replace do not allow to select specific subterms, whereas expand expects a name to be replaced. Bettina Buth ------------------------------------------------------------------------------ | Dr. Bettina Buth | Tel. : ++49-421-218-2955 | | FB 3 Informatik | Fax : ++49-421-218-3054 | | Bremen University, p.o. box 330 440 | email: bb@informatik.uni-bremen.de | | D-28334 Bremen, Germany | | ------------------------------------------------------------------------------

- Prev by Date:
**bug?** - Next by Date:
**Re: 2 Questions** - Prev by thread:
**Help** - Next by thread:
**Re: 2 Questions** - Index(es):