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

RE: PVS Problem



Dear Galina,

> Just a small question: I have my user-defined strategy. It works
> (thanks to your help). When I type it after the prompt "rule?" for
> each theorem, in the *pvs* buffer there are details from the proof (
> which I need for documentation purposes). In the case I use (C-c C-p
> U) or (M-x prut) commands a nice proof status appears, but in *pvs*
> buffer the proof details are missing.  Which command to use, that I
> have the user-strategy applied to all theorems in the .pvs file and
> also the proof details written in the *pvs* buffer/ .prf file?  I
> looked in the pvs-help, but didn't find anything helpful.

I'm afraid there's no way to do this using PVS in the normal,
interactive, way, but you can do it if you use PVS in batch mode.
This is described in Chapter 5 of the PVS User guide.  At verbose
level 3, batch mode produces full details of proof replays.  Note that
the inner details of proof strategies are not given (neither
interactively nor in batch) unless the strategies call their inner
strategies in their $ form, and are themselves called in their $ form
(see prover guide, page 14).  You may need to tinker with this to get
the level of detail you want.

I'm cc'ing this to the pvs-help list in case it's useful to others.

Regards,
John