Starting with HAHA

Installing required software

Java

HAHA requires JRE 1.8, 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-8-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. The download page provides stable binaries for Windows (both 32 and 64 bit), users of other systems must either

  • Use a nightly build, accessible by clicking ‘Planned’ under ‘Other downloads’ on the download page.
  • Or compile from source by following the procedure described below.

To compile Z3 from source, perform the following steps

  • 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 archives one for each of the 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. HAHA is typical file editor with standard and intuitve commands. One thing to keep in mind is that source files should have the extension .haha - toherwise the editor might not function properly.

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. This command can be also accessed from the main menu and the toolbar. 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.