Starting with HAHA

### Navigation

- index
- next |
- previous |
- HAHA 13/08 documentation »

# Starting with HAHA

## Installing required software

### Java

HAHA requires JRE 1.6, which can be downloaded from its website. Most Linux distribution also contain Java in their package repositories. On Debian and Ubuntu systems it can be installed with the following command:

    sudo apt-get install openjdk-6-jre

Note that it is not necessary to install the Java Development Kit (JDK), only the JRE is required to run HAHA.

### SMT solver

HAHA relies on a SMT solver to prove the validity of generated formulae. Currently the only supported solver is Microsoft Z3. It can be obtained from its Codeplex site. Binaries are provided for Windows (both 32 and 64 bit), users of other systems must compile from source. This can be achieved by following the procedure described below.

> - Download source code of the stable branch, either by clicking on the ‘Download’ link in the ‘Source code’ tab of the website or cloning the git repository at https://git01.codeplex.com/z3.

> - Unpack the source and enter the following commands:

>       autoconf
>       ./configure --prefix=/usr/local
>       python scripts/mk_make.py
>       cd build
>       make
>       sudo make install

> - Make sure that binaries are available on system `PATH`. The commands given here install binaries in `/usr/local/bin`, this can be modified by adjusting the `--prefix` option in the second line. In particular, it is possible to install Z3 in home directory, without root privileges.

Note

The compilation requires some additional software

> - C++ compiler (obviously)
> - autoconf
> - make
> - python

On Debian and Ubuntu systems, these can be installed with:

    sudo apt-get install autoconf make python g++

Note

In Mac OS X the standard C++ compiler is `clang++` (based on LLVM), rather than `g++` (GNU C++). Mac users should append the text `CXX=clang++` to the `configure` command.

Windows users can simply install the precompiled binaries from the website. It is still necessary to ensure that installed executables are available on the system `PATH`.

## Installing HAHA

HAHA is distributed as a single archive which contains builds for all supported systems. There is no installation procedure other than unpacking the directory containing the proper version from the archive. We provide both 32 (x86) and 64 (x86_64) bit variants of HAHA. It is necessary to choose the one that matches the version of Java available on the system. It can be obtained with the following command:

    java -version

Startup options can be configured in the `haha.ini` file found in the installation directory. Changing these options might be desirable in the following circumstances

> - In case of errors related to insufficient memory. This problem can be addressed by appending the following options to the config file

>   > - `-Xmx<total-memory-in-mb>m` (e.g. `-Xmx1024m`).
>   > - `-Xms<stack-memory-in-mb>m` (e.g. `Xms128m`).
>   > - `-XX:MaxPermSize=<permgen-memory-in-mb>m` (e.g. `-XX:MaxPermSize=512m`). Note that this value must be at least 256m for the IDE to work (512m is recommended).

> - If Unicode characters are not displayed correctly (especially in the outline view), append the following option:

>       -Dfile.encoding=UTF-8

Note

VM options must be given on separate lines, after the `-vmargs` line.

## Running

To run HAHA, launch the `haha` executable from the installation directory. At the first run, HAHA will present a window used to configure the workspace location. A workspace is simply a directory which will contain all HAHA source files.

Note

It might be a good idea to choose a location other than the default, to avoid conflicts with other variants of Eclipse (e.g. used for Java development).

Before any source files can be edited, it is necessary to create a project. This can be achieved by clicking the `File | New | Project...` menu item and choosing `General | Project` from the displayed tree.

Adding source files is similar to creating the project - choose `File | New | File` and type a filename, with `.haha` suffix.

Warning

HAHA sources will not be detected in files with extensions other than `.haha`.

The following sample can be pasted into the editor to verify that it is working correctly

    function hello() : Z
      postcondition hello = 4
      hello := 2 + 2

The code should be highlighted (assuming that the correct file extension was used). To start the verification process, right-click anywhere in the editor are and choose `Generate VCs` from the displayed menu. HAHA will then present a console with computed verification conditions and messages logged during verification. If there were any problems, error markers will be added to the editor.

### Navigation

- index
- next |
- previous |
- HAHA 13/08 documentation »