|
Abstract : |
John Rushby, and Dave Stringer-Calvert provided valuable input for the design of the evaluation capabilities in PVS. The work of Dave Greve, Dave Hardin, and Matt Wilding [HWG98] at Rockwell-Collins was the initial stimulus for the introduction of these features in PVS. Specification languages like PVS are designed to be expressive rather than executable. However, execution is useful for animating and validating specifications, and for automating certain kinds of proofs. A surprisingly large fragment of PVS turns out to be executable as a functional language with quite reasonable efficiency. Execution is achieved by generating Common Lisp code from PVS. The key step in generating efficient code is the use of static analysis to determine safe destructive array updates., |
