[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

- 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