Winter School: instruction for lab session/Krakatoa tool

There is a lecture about Krakatoa in the Winter School on Verification of Object-Oriented Programs.
This web page is dedicated to instructions for running the Krakatoa tool and doing exercises for the lab session. Krakatoa is one particular tool available inside the Why platform, so installing Krakatoa amounts to install Why. Moreover, the platform is able to call a family of external provers, which must be installed independently.

Lectures
Exercices
Installing Provers
Installing Krakatoa
Eclipse Plugin

Please report installation problems but also successful installation to Claude Marché

Lectures

Lecture 1: Slides, Isqrt.java, Purse.java, Sort.java
Lecture 2: Slides, Muller.java
Lecture notes

Exercices

Claude Marché

Power function: PDF, HTML, source file
Greatest common divisor: PDF, HTML, source file
Binary search: PDF, HTML, source file
Electronic purse: PDF, HTML, source file
Dijkstra's Dutch Flag: PDF, HTML, source file
Mystery code: PDF, HTML, source file
Translation rules: PDF, HTML

Installing Provers

Please install as many provers as possible from the following list, and at least Simplify and Alt-ergo.

Simplify (version 1.5.4): is available under binary form for various architectures from this page or directly here
Alt-Ergo (version 0.8): is available under binary form for Unix, or under source form to be compiled using the OCaml compiler, from this page. A Microsoft Windows installer (for version 0.7.3) is also available on this page
Z3 (version 1.3): is available under binary form for Microsoft Windows from this page. Running this program under Unix is also possible via the wine layer: install z3 using the msiexec command and then run it using this script where you have to modify the full path to z3.exe
Yices (version 1.0.17): available under binary form for various platform from this page
CVC3 (version ): available under source form and as a Unix binary from this page

Note: for use of proof assistant such as Coq or PVS, see why web page. Only automatic provers will be used during the school.

Installing Krakatoa

Krakatoa is primarily developed for running under Unix platforms. Some partial support is also provided for Microsoft Windows. It is recommended to install the new version 2.18 of Why and Krakatoa

Precompiled binaries

Installing a precompiled binary is of course much easier, but may fail if your architecture is not well supported.

Unix/Linux binary distribution is available as this tarball. You must uncompress it in a temporary directory, and then type "./configure" followed by "make install". This will install in directory "/usr/local/bin" and "/usr/local/lib" by default, hence superuser privilege is required for install. Installation in alternative directory can be done using option "--prefix" of "./configure", e.g. "./configure --prefix=/home/myname"
a Windows installer is available for the Frama-C platform which includes Why 2.17, thus providing a usable replacement for Why 2.18 if compilation of sources is not successful.

Compilation from sources

Compilation from sources amount to uncompress the sources and do

./configure
make
sudo make install

See remarks above for changing the default destination directory.

This will work only if proper development tools are installed first:

The Objective caml compiler
The Lablgtk Library

Here are some hints to setup a proper environment:

Under Debian-based distributions, those can be obtained by installing packages "ocaml", "ocaml-native-compilers" and "liblablgtk2-gnome-ocaml-dev"
Under other Unixes, a simple solution is to install those via the godi system
Under Microsoft Windows, the sources can be compiled under the cygwin environment. Note that the MinGW version of the Objective Caml compiler should be installed.

Testing installed Krakatoa

To test your installation, you should run

gwhy Isqrt.java

on that Isqrt.java file and in the GUI, click on buttons "Simplify" and "Alt-Ergo" at top of columns of the table on the left. You should obtain the following:

Eclipse plugin

For Eclipse fans, there is an Eclipse Plugin for the Why platform. Note that a few minor features are missing w.r.t to the dedicated GWhy interface.

30/1/2009