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

[PVS-Help] Re-running proof does not update proof status in *.prffile



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