Examples
========

.. highlight:: haha

Here is a number of examples that illustrate a few specific features
of the HAHA language.

.. _cubicroot:

Cubic root
----------

.. literalinclude:: cubic-root.haha

The Z3 solver that is used as the proving backend for the tool
supports well arithmetic with frequent addition. Therefore, we need
to add additional information that helps the solver to complete the
Hoare logic proofs in this example. This is done with axioms. They are
introduced with ``axiom`` keyword and can be named as it is in the
case of preconditio, postcondition or axiom.

The assertions can span over many lines, which can be observed in
the loop body of the example::

  		y := y + 3*a + 3*b + 1 // y := (b + 1) ^3
  		{ (b ^ 3) <=  x /\ y = (b + 1) ^ 3 /\ 
  		  a  = b ^ 2  /\ x >= 0 }
  		a := a + 2*b + 1

We can also supply additional comments that provide additional
explanation for particular assertions or pieces of code::

  		y := y + 3*a + 3*b + 1 // y := (b + 1) ^3

Here, we inform that the assignment is in fact the assignment of
the cubic power of ``b + 1`` to ``y``.

.. _exponentiation:

Exponentiation
--------------

.. literalinclude:: exponent.haha

This example shows that we can give function multiple
parameters. Unlike Pascal we require programmers to give full type
specifications in case multiple parameters of the same type are
necessary. Therefore, the header of the exponent function is::

  function power( y : Z, x : Z ) : Z

Another important feature of the program is that we use here a simple
predicate. The predicate is introduced with the keyword ``predicate``
and its header is similar to the one of function except that the
result type is not given as it does not make sense here. The header of
the predicate definition is followed by ``=`` sign and the definition
of the predicate body. In our case this is::

  predicate odd(x : Z) = (x mod 2 = 1)

We can see here a number of axioms that are necessary to make the
proof go through.

* The axiom ``tozero`` makes it possible to draw the final conclusion
  from the exit condition of the while loop. The condition holds when
  ``q`` is zero and then the invariant condition gives the required
  result provided that we know the meaning of exponentiation to the
  power of zero.

* The axiom ``odddiv2`` is necessary to understand that odd powers
  decompose in a particular way when divided by 2. This formula is
  necessary to make proof go through the instruction ``q := q / 2``.

* The axioms ``twoinexp`` and ``twoandoneinexp`` are necessary to
  understand how even and odd powers turn to multiplication. This is
  again necessary for the proof of the instruction ``q := q / 2``.


.. _binarysearch:

Binary search
-------------

.. literalinclude:: binary-search.haha

This example illustrates the way we handle arrays. The array parameter
declaration in predicates and functions looks as follows::

  predicate ordered( A : ARRAY [Z], i : Z, j : Z ) = ...
  function bsearch( A : ARRAY [Z], len : Z , v : Z ) : Z 

One important thing to note here is that the arrays in our language
have infinite domain of keys, namely the whole integer numbers ``Z``.
Therefore, we need to introduce explicit parameter that describes the
range of the array to make the verification similar to the real-world
situation. In this example we decided that the arrays range from ``1``
to some number held in the parameter ``len``.

This example also illustrates how well chosen set of predicates may
make the verified procedure very nicely and comprehensively
documented.


.. _partition:

Quicksort partition
-------------------

.. literalinclude:: partition.haha

This example serves to demonstrate how the features such as predicates
and invariant labelling work in bigger examples. First, the predicates
make it possible to exchange long and obscure expressions that define
particular features into insightful labels. Second, the complicated
invariant formula can be divided into meaningful pieces that describe
a particular aspects of the loop invariant, which also contributes to
readability. It is important to understand that the split does not
mean that the reasoning about the pieces is separate. In particular we
need the information on guards to correctly establish the new version
of ``sides`` part.

We have to make one important point. It is critical to split the
invariants when they become so big since it is very difficult without
this to figure out what is wrong in case some subtle mistake is done
either in the code of the program or in the assertion
formula. Splitting of the conditions helps to localise the problem.