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.
## Proving
program correctness

Currently proof obligations can be generated
for
The Jack proof manager sends the proof
obligations to the different provers, and keeps track of proven and
unproven proof obligations.
## More information

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.

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 ').