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

*To*: Perry.Alexander@UC.EDU*Subject*: PVS dump files*From*: Steve Johnson <sjohnson@cs.indiana.edu>*Date*: Tue, 23 Feb 1999 13:24:45 EST*cc*: psm@cs.indiana.edu (Paul S. Miner), pvs-help@csl.sri.com

Perry, 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?

- Prev by Date:
**Re: Quantifiers** - Next by Date:
**Re: PVS dump files** - Prev by thread:
**Re: library path** - Next by thread:
**Re: PVS dump files** - Index(es):