[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: questions about pvs...
Appologies in advance. I haven't taken the time to verify the
correctness of my answers....
> 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.
It won't work. PVS doesn't load the strategies.lisp file. (I say
this because there have been releases where the file hasn't been
included, but PVS still ran fine)
> 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??
All this code is in
you may also wish to look at
It wasn't immediately obvious to me how to do what you're asking for.
But if you figure it out, we'd certainly be interested in it.
> thanks for your help,
Hope this helped you some.
John Hoffman, PhD ||
Secure Computing Corporation || Sushi is good?
2675 Long Lake Road || Life is good!
Roseville, MN 55124 ||
Fax :(612)628-2701 || - Origami Sushi Chef