Krakatoa Verification Tool for JAVA programs Tutorial and Reference Manual
Krakatoa is a tool for certification of Java programs, annotated using the Java Modeling Language [4] (JML for short), using the Why [1] tool for generating proof obligations. This version 1.11 of Krakatoa is a major rewriting of the version 0.x family. Major changes have occured 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. We present the language of expressions one can use in annotations. These are called logic expressions. This language is essentially the standard multi-sorted first-order logic. It is a two-valued logic language, made of propositions with standard first-order connectives, built upon a language of atoms called terms.
As far as possible, the syntax of Java expressions is reused: conjunction is denoted as &&, disjunction as || and negation as !. Additional connectives are ==> for implication, <==> for equivalence. Universal quantification is denoted by \forallτ x1,…,τ xn;e and existential quantification by \existsτ x1,…,τ xn;e.
Terms are built on
• integer and real arithmetic
• Java array access and field access
• Java cast
• user-defined logic types, and user-defined predicate and logic functions
Get pdf download Krakatoa Verification Tool for JAVA programs Tutorial and Reference Manual
Related Tutorial
Tags: access java, disjunction, equivalence, existential quantification, java array, java cast, java objects, java programs, jml, krakatoa, logic functions, logic language, memory heap, negation, predicate, proof obligations, reference manual, universal quantification, verification tool, xn
Comments
Leave a Reply