Java Applet Correctness Kit: a tutorial
This document constitutes a tutorial to the JACK tool. JACK is an eclipse plugin allowing to ensure the correctness of Java application annotated with JML. The version of the tools referenced in this document are :
– Jack v1.8.0
– eclipse 3.1
You need to have eclipse installed and to have access to a Jack update site, then you install the plugins using the classical eclipse framework. Independtly you need to install the provers you want to use. The different available provers are:
– B: you can choose to install the Atelier B or the B4Free toolkit.
– Coq: you need to have coq installed and also an interactive proof interface: coqIde, pcog, proofgeneral.
– PVS: you need to have PVS installed and also emacs or xemacs
– Simplify: you need to install the simplify prover by getting the executable on the ESC-Java web site.
Get pdf download Java Applet Correctness Kit: a tutorial
Related Tutorial
Tags: correctness, eclipse plugin, emacs, interactive proof, interface, java applet, java application, java web, provers, toolkit, v1, xemacs
Comments
Leave a Reply