PVSio

PVSio is a PVS package that extends the ground evaluator with a predefined library of imperative programming language features such as side effects, unbounded loops, input/output operations, floating point arithmetic, exception handling, pretty printing, and parsing. The PVSio input/output library is implemented via semantic attachments. PVSio has been part of PVS since PVS 5.0. The current version of PVSio is 6.0 and is included in PVS 6.0. PVSio 6.0 provides: A standard library of semantic attachments. A high level interface for writing user-defined semantic attachments. A simpler Emacs interface and a stand alone Emacs-free interface to the ground evaluator. The proof commands eval-expr and eval-formula that safely integrate the ground evaluator into the PVS theorem prover. These proof rules use the efficient Common Lisp code generated by the ground evaluator to simplify ground expressions in sequent formulas.