The Jack tool provides an environment for verification of Java and
Java Card programs with
JML
annotations. It implements a fully automated weakest precondition
calculus that generates proof obligations from annotated Java
sources. Those proof obligations can be discharged using different
theorem provers.
JML verification for Java developers
An
important design goal of Jack is that it is easy to use for normal
Java developers, who use it to validate their own code. To allow
developers to work in a familiar environment, Jack is integrated as a
plugin in the
eclipse IDE. Care has
been taken to hide the mathematical complexity of the underlying
concepts. Therefore Jack provides a dedicated
proof obligation viewer, that presents
the proof obligations connected to execution paths within the
program. For each proof obligation, the relevant source code is
highlighted. Moreover goals and hypothesis are displayed in a Java/JML
like notation.
Our goal is to allow formal method experts to prove the correctness of
Java applets, and moreover, to allow Java programmers to obtain a high
confidence in the correctness of their application.
Proving
program correctness
Currently proof obligations can be generated
for
- The
Simplify
theorem prover, notably used by ESC/Java.
- The Coq proof
assistant.
The
Jack proof manager sends the proof
obligations to the different provers, and keeps track of proven and
unproven proof obligations.
More information
Jack has been initially developed by the Research Laboratory at Gemplus and is now
being developed within the Everest team
at INRIA Sophia Antipolis, with partial support from the IST project
INSPIRED, and of the ACI
Sécurité GECCOO.
Jack is publicly available under a Cecill C
licence.
If you want to keep in touch with Jack developements you can subscribe
to the
jack-interest@lists-sop.inria.fr mailing list.
To do so,
simply send an email to sympa@lists-sop.inria.fr
with the subject line 'subscribe jack-interest' (without the ').