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

*To*: Steve Johnson <sjohnson@cs.indiana.edu>*Subject*: Re: PVS dump files*From*: Perry Alexander <alex@ececs.uc.edu>*Date*: 24 Feb 1999 11:42:15 EST*cc*: psm@cs.indiana.edu (Paul S. Miner), pvs-help@csl.sri.com*In-Reply-To*: Steve Johnson's message of "Tue, 23 Feb 1999 13:24:45 -0500 (EST)"*References*: <199902231824.NAA00677@bulldog.cs.indiana.edu>

Steve Johnson <sjohnson@cs.indiana.edu> writes: > 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? This is pretty much what I do. I have the students dump the theory representing their work to a file, then email me the result. When I'm grading I undump the file and run prove-pvs-file. The result tells me the status of each attempted proof. It's virtually automatic for the first few homeworks, but as they get more complex I have to poke around more. The only catch is when someone accidentally tries to prove an axiom, it shows up as an incomplete proof. Not at all a big deal though. I don't know of any way to include the student's .pvscontext file in this process that's not a hack. However, I can't recall any time that prove-pvs-file has ever proven a theorem that the student didn't actually attempt a proof for. I usually want to see the proof run anyway because I restrict the set of commands available to students on some homeworks. Given how I restrict the available commands, it would be pretty easy to tell if PVS provided the proof instead of the student. - Perry -- Dr. Perry Alexander / ECECS Dept. / The University of Cincinnati PO Box 210030 / 896 Rhodes Hall / Cincinnati, OH 45221-0030 513.556.4762 (Voice) / 513.556.7326 (FAX) perry.alexander@uc.edu / http://www.ececs.uc.edu/~alex

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