[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
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
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.