[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: PVS dump files
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