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 and is included in the latest release of PVS. PVSio provides:
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