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:
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.