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

*To*: pvs-help@xxxxxxxxxxx*Subject*: [PVS-Help] Re-running proof does not update proof status in *.prffile*From*: "Thomas Wilson" <thomas@xxxxxxxx>*Date*: Wed, 23 May 2007 15:34:30 +0100 (BST)*List-Help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-Id*: PVS-Help <pvs-help.csl.sri.com>*List-Post*: <mailto:pvs-help@csl.sri.com>*List-Subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-Unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx*User-Agent*: SquirrelMail/1.4.5

Hi, I am using PVS version 3.1 (Feb 14, 2003) to prove Verification Conditions generated by my verification tool. I generate PVS theories with the conjectures, along with *.prf files with initial proof attempts. Currently these initial proofs are simply '(grind)' which along with the auto-rewrites can prove some simple VCs automatically. I flag their proof status as 'untried' initially. My tool reads the *.prf files to allow the user to track the progress of PVS proofs together with the details of the other forms of verification. My idea was to 're-run' these initial proofs for each theory to discharge any trivial VCs before interactively proving the remainder of the VCs. I can do this using prove-theory and the initial proofs do work sometimes but PVS does not update the details of the proofs in the *.prf file. I had expected it to change the status of the proofs to be 'proved' if the proofs succeed but they remain 'untried' despite being reported as 'proved' by display-proofs-theory. It only seems to update the *.prf file if I re-do a proof manually from scratch. At that point it also updates the details of the other proofs and updates successful initial proofs to 'proved'. I also get the same problem when I manually edit a *.prf file to copy portions of a proof from one VC to another. PVS will accept the new proof script but, again, it doesn't write back to the *.prf file that it is proved. How can I get PVS to update the details of my non-PVS-generated proofs when I re-run them? Is there a workaround that you could suggest? If all the VCs in a file are proved by the initial proof attempts, the only way I can get PVS to update the *.prf file is to arbitrarily re-prove one of the VCs manually. In the latest file I have been working on, I had to interactively verify all the VCs and I copied parts of the script from one proof to another. PVS again accepts the proofs and reports them as 'proved' in display-proofs-theory but won't update the *.prf file. I don't want to have to manually re-enter one of the long proofs in this file to force an update of the *.prf file! I don't really want to have to manually set the proof status of proofs to be 'proved' myself either, I would rather PVS did that. I would be grateful for any advice you could give me. Thanks, Thomas

- Prev by Date:
**Re: [PVS-Help] Simple (?) question on PVS - constants offunctions of other constants** - Next by Date:
**Re: [PVS-Help] Re-running proof does not update proof status in *.prffile** - Prev by thread:
**Re: [PVS-Help] Re-running proof does not update proof status in *.prf file** - Next by thread:
**Re: [PVS-Help] Re-running proof does not update proof status in *.prffile** - Index(es):