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é
Solutions are available on demand to 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
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.
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:
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