.. _langref: 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 ----------------- .. figure:: grammar/Program.* :scale: 150% :align: center 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. .. figure:: grammar/Function.* :scale: 75% :align: center .. figure:: grammar/ArgumentList.* :scale: 150% :align: center .. figure:: grammar/Argument.* :scale: 150% :align: center .. figure:: grammar/Precondition.* :scale: 150% :align: center .. figure:: grammar/Postcondition.* :scale: 150% :align: center .. figure:: grammar/Locals.* :scale: 150% :align: center .. figure:: grammar/Local.* :scale: 150% :align: center 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. .. figure:: grammar/Predicate.* :scale: 150% :align: center 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 :ref:`binarysearch` and :ref:`partition`. .. figure:: grammar/Axiom.* :scale: 150% :align: center 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 :ref:`cubicroot` and :ref:`exponentiation`. Types ----- .. figure:: grammar/Type.* :scale: 150% :align: center .. figure:: grammar/SimpleType.* :scale: 150% :align: center .. figure:: grammar/PrimitiveType.* :scale: 150% :align: center .. figure:: grammar/ArrayType.* :scale: 150% :align: center 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 ------------- .. figure:: grammar/HoareTriple.* :scale: 150% :align: center .. figure:: grammar/AssertionList.* :scale: 150% :align: center .. figure:: grammar/TrailingAssertionList.* :scale: 150% :align: center .. figure:: grammar/Assertion.* :scale: 150% :align: center 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. .. figure:: grammar/Statement.* :scale: 150% :align: center .. figure:: grammar/SimpleStatement.* :scale: 150% :align: center .. figure:: grammar/CompositeStatement.* :scale: 150% :align: center .. figure:: grammar/Skip.* :scale: 150% :align: center .. figure:: grammar/Assignment.* :scale: 150% :align: center .. figure:: grammar/Block.* :scale: 150% :align: center .. figure:: grammar/Cond.* :scale: 150% :align: center .. figure:: grammar/Loop.* :scale: 150% :align: center .. figure:: grammar/LoopInvariant.* :scale: 150% :align: center 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 ----------- .. figure:: grammar/Expression.* :scale: 150% :align: center .. figure:: grammar/Equivalence.* :scale: 150% :align: center .. figure:: grammar/Implication.* :scale: 150% :align: center .. figure:: grammar/Disjunction.* :scale: 150% :align: center .. figure:: grammar/Conjunction.* :scale: 150% :align: center .. figure:: grammar/Negation.* :scale: 150% :align: center .. figure:: grammar/Quantifier.* :scale: 100% :align: center .. figure:: grammar/ForallVar.* :scale: 150% :align: center .. figure:: grammar/Comparison.* :scale: 150% :align: center .. figure:: grammar/Sum.* :scale: 150% :align: center .. figure:: grammar/Product.* :scale: 150% :align: center .. figure:: grammar/Power.* :scale: 150% :align: center .. figure:: grammar/Uminus.* :scale: 150% :align: center .. figure:: grammar/ArrayAccess.* :scale: 150% :align: center .. figure:: grammar/Atom.* :scale: 150% :align: center .. figure:: grammar/Call.* :scale: 150% :align: center .. figure:: grammar/Var.* :scale: 150% :align: center .. figure:: grammar/ActualArgs.* :scale: 150% :align: center .. figure:: grammar/IntLiteral.* :scale: 150% :align: center .. figure:: grammar/BoolLiteral.* :scale: 150% :align: center .. figure:: grammar/Bool.* :scale: 150% :align: center 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.