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

Executing PVS

Hello all,

I talked with John Rushby at FME about my plans to use the decision
procedure library as a part of a compiler, and he mentioned that PVS
can also be used as a programming language. This prompted me to look
for the following report:

    N. Shankar. Efficiently executing PVS. Project report,
    Computer Science Laboratory, SRI International, Menlo Park,
    CA, November 1999. Available at 
http://www.csl.sri.com/shankar/PVSeval.ps.gz .

Unfortunately the link is broken, so would some kind soul at SRI
fix it please?

I am planning to write a compiler for a specification language based
on superposition. The input for the compiler is a list of superposition
steps and instructions on how they should be composed. The output is
a single joint action specification, i.e. temporal logic + objects.

Would it be practical to write the compiler in PVS? The syntactic
manipulations involved are pretty straightforward, and I would need
to write them as recursive functions in PVS anyway if I want to reason
about the compiler. The compilation process involves some reasoning
about action implications (predicate logic reasoning), so I guess
I would get the proof obligations for free were I to implement the
compiler in PVS.

If anyone has experiences to share with me, I would be very grateful.