[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS] PVSio: Rapid Prototyping in PVS



Announcement: Release of PVSio.2a
---------------------------------

Freely available at http://research.nianet.org/~munoz/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
library is implemented via semantic attachments. 

PVSio is extensible as it provides a high level interface for writing
user-defined semantic attachments. It also provides a simpler Emacs
interface and a stand alone Emacs-free interface to the ground
evaluator. 

Finally, PVSio includes proof rules that safely integrates the ground
evaluator to 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.

Comments and bug reports are welcome,

Enjoy it,

Cesar

-- 
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
National Institute of Aerospace      mailto://C.A.Munoz@larc.nasa.gov
144 Research Drive                  http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 766 1539 Fax +1 (757) 766 1855