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

questions about pvs...


I've been working on using PVS to reason about the proofs of ASTRAL
real-time specifications.  I've encoded ASTRAL into PVS and written a
translator and now I'm trying to develop some general techniques and
PVS strategies to make the user's life easier.

One thing I've noticed is that some of the TCCs that are not finished off
by the tcc strategy could have been if it only had access to a few rewrite
rules of the encoding.  I would like to add these to the tcc mechanism and
was wondering what the "cleanest" way to do this was and/or if there was a
particular way the PVS designers had in mind.  I know the tcc strategy
can be redefined in the pvs-strategies file, but I don't know if the tcc
mechanism loads user strategies before it starts or not.  I'm sure the
strategies.lisp file could also be modified, but that certainly doesn't seem
very elegant.

I was also wondering how easy it would be for me to add a procedure similar to
the "prove" part of "typecheck-prove".  That is, I will have a theory that
just consists of a bunch of theorems that are not necessarily true and want to
use a single command to attempt the proofs of all of them using the same
predefined strategy.  If the strategy generates subgoals that can't be proven,
then I'd just like it to indicate "unfinished" like the tcp procedure.
It seems like I could just copy the tcp code and replace the tccs file with
my theory file and the tcc strategy with my strategy and add the command to
the "pvs-cmds.el" file.  What I don't know is if the tcp code is actually
available anywhere to copy and incorporate.  So can you tell me if this is
possible and if so, where I might find the tcp code??

thanks for your help,

--Paul Kolano