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.
Read more

• Recently Written

  • HTML5 WebSocket & Communication
  • Does HTML 5 Herald The End Of RIA Plug-Ins? Not Really
  • HTML5 Programming Fast Track
  • Safari HTML5 Audio and Video Guide
  • HTML5 Quick Learning Guide
  • Xcode User Default Reference
  • Xcode Debugging Guide (Tools & Languages: IDEs)
  • Xcode Installation Guide (Tools & Languages: IDEs)
  • Xcode Build System Guide (Tools & Languages: IDEs)
  • Programming with Google Android and Eclipse

• Categories

  • Ada
  • Algorithrm
  • ASP.NET
  • assembly
  • C#
  • C/C++
  • Caml
  • ColdFusion
  • CORBA
  • Database
  • General
  • Hardware
  • Java
  • Javascript
  • MAPI
  • News
  • Oracle
  • Perl
  • PHP
  • PostScript
  • Python
  • Ruby
  • SAP
  • Scripting
  • Silverlight
  • Tools
  • VBA
  • Visual Basic
  • XML

• 
  
• Archives

  • July 2010
  • June 2010
  • May 2010
  • March 2010
  • February 2010
  • January 2010
  • December 2009
  • November 2009
  • October 2009
  • September 2009
  • August 2009
  • May 2009
  • April 2009
  • March 2009
  • February 2009
  • January 2009
  • December 2008
  • November 2008
  • October 2008
  • September 2008
  • August 2008
  • July 2008
  • June 2008
  • May 2008
  • April 2008