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

Re: [PVS-Help] Changing a goal formula



On Tuesday 28 June 2005 00:19, Erika Rice wrote:
> As part of a strategy, I want to replace a formula in the goal goal
> with another formula.  Currently, I am using
>     (setf (formula (car (select-seq (s-forms *goal*) fnum))) new-formula)
> However, this has the disadvantages that
>     1. My strategy acts like a skip (which makes using try/else
>       impossible)
>     2. I cannot use undo after applying the strategy
>
> Is there a proper way of manipulating a goal formula?  If not, is
> there some way I can get around the problems above (esp. #1)?

Directly replacing formula objects is unwise in my opinion.  How do you know 
the replacement is sound?  How do you know there isn't some pointer to the 
old formula still in use? 

I suggest using the strategy features more conservatively.  My approach is to 
use Lisp code to extract information from the current sequent, but when it 
comes time to take action, I invoke normal prover rules (from within the 
strategies) to carry out desired actions.  This might involve creating new 
PVS terms (as text) and letting the prover parse them.  It's a bit slower but 
safer because the prover does all the usual checking for you.

If you haven't seen it yet, you might want to look at the proceedings of a 
recent workshop on PVS strategies:

http://library-dspace.larc.nasa.gov/dspace/jsp/bitstream/2002/14474/1/NASA-2003-cp212448.pdf

It includes two tutorials and several papers on various aspects of writing 
strategies.

Ben