Introduction

HAHA is a programming language embedded in a modern program development environment based on Eclipse. The purpose of HAHA is to teach students Hoare logic. A programmer can write simple programs and annotate them with Hoare logic assertions. The environment verifies the assertions against the code and discharges them with help of external theorem provers, both automated and interactive. A user can write programs that manipulate on true integers and on arrays.

This document describes version 0.56 of HAHA. It serves as a user manual. It contains instructions on how to start using the tool, a gentle introduction the HAHA language, a description of the outputs served by the environment, language reference, and a set of more complicated examples.

This document is not meant to serve as a developer manual. Details of the design of the tools and description of how to effectively adapt the tool to the needs of a particular formal methods course are presented elsewhere.

Availability

You can download the newest version of the program from http://haha.mimuw.edu.pl/

Contact

You can contact the authors through the email haha@mimuw.edu.pl.

Acknowledgements

The project was partly financed by Polish government grant N N206 493138 and NCN grant no 2013/11/B/ST6/01381. We are grateful Andrzej Tarlecki for continuous mental support for the project.

Requirements

• Java 1.8
• Microsoft Z3
• The program is actively tested on Windows 8, Linux Fedora 24. In principle it should also work on other Windows or Linux based operating systems.

Note

We no longer provide binaries for Mac OS X, since we do not have available testing resources.