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
JML verification for Java developers
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
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.
Currently proof obligations can be generated
theorem prover, notably used by ESC/Java.
- The Coq proof
The Jack proof manager
sends the proof
obligations to the different provers, and keeps track of proven and
unproven proof obligations.
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
Jack is publicly available under a Cecill C
If you want to keep in touch with Jack developements you can subscribe
firstname.lastname@example.org mailing list.
To do so,
simply send an email to email@example.com
with the subject line 'subscribe jack-interest' (without the ').