Language reference

This section contains a complete description of HAHA syntax. All language constructs are presented using syntax diagrams.

Lexical conventions

The following list specifies base lexical elements from which HAHA programs are composed.

• Whitespace, which is only used to separate other elements.
• Comments - both single line (// ...) and multiline (/* ... */). Multiline comments cannot be nested.
• Keywords and operators (specified in single quotes in the following text).
• Identifiers (ID), which consist of letters (a to z), digits and underscores. Identifiers cannot start with a digit.
• Numbers (BIGINT) - sequences of digits, leading zeros are not allowed.
• Strings (STRING) - which are used for documentation purposes only (there is no string type in the language). Strings are specified in qither double or single quotes, both variants support a set of escape sequences (e.g. “”” is a string consisting of a quote character).

Program structure

Each HAHA source file contains a single program, which is a list of top-level elements. A top-level element can be a function, a predicate or an axiom.

A function definition consists of

• Name.
• List of argument names and types.
• Result type.
• Optional documentation strings.
• Preconditions and postconditions
• Local variable declarations (each variable has name, type and an optional docstring).
• Function body.

A predicate is a named and parameterized boolean expression. Use of predicates can be very helpful in making a program readable. This is especially true when dealing with arrays, as in examples Binary search and Quicksort partition.

Axioms are simply boolean formulae that can be optionally named for clarity. Axioms are typically used when the automated solver is unable to prove a valid formula. Examples that make use of axioms include Cubic root and Exponentiation.

Types

Basic types used in HAHA programs are true integers Z and multi-dimensional arrays. Booleans are also supported. The syntax also includes a primitive type Int, which is supposed to represent 32 bit integers, but support for that type is incomplete in current version of HAHA.

Hoare triples

A Haore triple is a statement with a list of precondtions and postconditions. One peculiarity of the HAHA syntax is that a semicolon is necessary to terminate the list of preconditions, unless that list happens to be empty.

Statements available in HAHA include

• The skip statement.
• Assignment - this includes assignment of the function result, which is represented by a special variable with the same name as the containing function.
• Blocks - lists of statements separated by midconditions.
• Conditional statements, with an optional else part.
• While loops. Loops are annotated with (optionally named) invariants and counter formulae. Counter formulae are used to prove termination of a program. This is an experimental feature and is not described in this documentation.

There are some ambiguities in the concrete syntax corresponding to the diagrams presented hare. First, there is the dangling else problem, which is resolved by matching every else to nearest open if. Second issue arises when a statement, such as if or while, ends in a Hoare triple. If hat statement is itself a part of a Hoare triple, it might not be clear if trailing assertions should become a part of the inner or the outer triple. By default, the inner triple is chosen.

Expressions

HAHA supports a number of traditional boolean and integer operators. It should be noted that many operators can be written in multiple variants. For example, conjunction can be represented as ∧ (Unicode character), /\ (Coq style) or simply and.

Supported operators include

• Logical operators: iff, implication, conjunction, disjunction, negation.
• Quantifiers (forall and exists).
• Integer comparisons.
• Integer operations: addition, subtraction, multiplication, division, remainder and exponentiation.

Quantified formulae may contain declarations of instantiation patterns. These patterns are used by the solver to decide when to create instances of a quantified formula. A pattern should contain all variables bound by the quantifier. For further discussion of the instantiation pattenrs, refer to the documentation of Simplify or Z3 solvers.

Note

Function calls are not supported by the current version of HAHA.