Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Krakatoa
NewsDownloadExamplesRelated publicationsOther links
The Krakatoa Tool for Java Program Verification
The Java
Modeling Language, JML for short, has been designed to formally
specify the behaviour of Java programs. The Krakatoa tool allows one
to certify that a JML-annotated method of a Java program meets
its specifications. More precisely, it focuses on verifying the
soundness of implementations with reference to pre/post-conditions
(given in the specification) and class invariants. This amounts to
proving that class invariants, as well as post-conditions, hold at the
end of a method execution, provided that invariants and pre-conditions
were valid at the beginning.
The Krakatoa approach involves three distinct components: the Why tool, which computes proof
obligations for a core imperative language annotated with pre and post
conditions, the Coq proof assistant
for modelisation of specifications and development of proofs, and
finally the Krakatoa tool, which reads the Java files and produces
specifications for Coq and a representation of the semantics of the
Java program into Why's input language.