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

PVS dump files


I'm having students turn in PVS dump files for homework exercises.  I deposit
them in a different subdirectory for each student.  I'd like to do the
following with a given student's file:

       Undump the dumped files
       Check the proof status of formulas therein with respect to the .prf file 

If I simply do a proof-status on the .pvs file, all formulas are listed as
unproved.  If I do a prove-file, PVS redoes the proofs that the student
turned in, but also autonomously proves other formulas.  I've fiddled with
other commands, but nothing seems to reinstate the context as the student
had it.  Any suggestions?