Krakatoa is a tool for certification of Java programs, annotated using the Java Modeling Language [5] (JML for short), using the Why [1] tool for generating proof obligations.
This version 2.34 of Krakatoa is a major rewriting of the version 0.x family. Major changes have occurred including changes in the syntax of annotations.
Chapter 2 is a tutorial to introduce the user step by step to the use of Krakatoa.
Chapter 3 is a reference manual where all options of the tool are described, and also the modeling of Java objects and Java memory heap, that you may encounter if you discharge proofs interactively, e.g. using Coq.
In the appendix you will find various additional informations, including the requirements, a summary of known limitations, and how to get help.
The use of the Why2 VC generator is now obsolete, and it is recommended to switch to the Why3 system for specification and VC generation. Why3 must be installed independently of Why2, please instructions given at http://why3.lri.fr.
The version of Why3 that is compatible with this version 2.30 of Krakatoa is the version 0.71. Please see http://krakatoa.lri.fr/ for more details on compatibility between Why2/Krakatoa and Why3.
In this manual, it is assumed that the Why3 VC generator and IDE is in use. The old behavior using the Why2 VC generator and GUI remains possible, using the gwhy command just as in version 2.29.