[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.

It does.

>   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 

emacs/pvs-cmds.el

you may also wish to look at 

emacs/pvs-prover.el

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


==============================++======================
John Hoffman, PhD             ||                    
Secure Computing Corporation  || Sushi is good?
2675 Long Lake Road           ||     Life is good!
Roseville, MN  55124          || 
hoffman@securecomputing.com   ||                    
Fax  :(612)628-2701           ||  - Origami Sushi Chef
Phone:(612)628-2808           ||                    
==============================++======================