Gentle introduction to HAHA language

Suppose that we want to write a function that given a number n returns the sum of all subsequent numbers from 1 to n inclusively. We start with a header of the function:

function sum( n : Z ) : Z

it contains the keyword function that tells the system to interpret the following expressions as a function. Then the name of the function is given, in this case it is sum. The information about its parameters is enclosed in the parenteses. In our case, we have one formal parameter that is called n. We declare the type of the parameter after the colon. It is Z this time, i.e. the type of integer numbers as we know them from mathematisc (these are not 32-bit integer numbers frequently met in programming languages). In the end, the parentesis with parameters is followed by the declaration of the result type. In our case this is again Z.

This function header can be followed by the definition of the body. The header with the body together look as follows:

function sum( n : Z ) : Z
begin
     x := 1
     y := 0
     while x <= n do
     begin
             y := y + x
             x := x + 1
     end
     sum := y
end

The code should not be surprising as we have all seen at least one implementation of the sum in our lives, especially for those who are familiar with Pascal as much of the syntax is based upon the language. However, let us discuss the details of the definiton to feel at ease in further development of other programs. First of all, the code as it stands is not syntactically correct. We assume in our language that all variables that are used in code must be declared beforehand. Therefore, we need to add between the function header and body declarations of the variables x and y so that the code is as follows:

function sum( n : Z ) : Z
var x : Z
    y : Z
begin
     x := 1
     y := 0
     while x <= n do
     begin
             y := y + x
             x := x + 1
     end
     sum := y
end

The keyword var, as in Pascal, marks the beginning of variable declaration sequence. Unlike Pascal, the elements of the sequence are not separated with semicolons ;, but with newlines. This holds both for variable declarations and instructions.

The variable assignemt is done in the Pascal style as in:

x := 1

or:

y := y + x

We also use the Pascal style to define the return result of the function, i.e.:

sum := y

The while loop is defined by a phrase of the form:

while x <= n do

followed by an instruction the loop iterates over. In our case this is a block instruction enclosed between begin and end, i.e.:

begin
        y := y + x
        x := x + 1
end

To express our intent with regard of the function we can add a precondition and postcondition formulae. These are located between the function header and its body. This looks as follows in this case:

function sum( n : Z ) : Z
precondition n >= 1
postcondition sum = n * (n+1) / 2
var x : Z
    y : Z
begin
...

In this case the precondition, introduced with precondition keyword, says that the function can be called when the parameter n is not less than 1. The postcondition, introduced with postcondition keyword, says that the result is equal to the commonly known (oh, our Gauss heritage) closed formula for the sum of the integers from 1 to n. These conditions can be named to make future reference easier:

precondition natural: n >= 1
postcondition gauss: sum = n * (n+1) / 2

Hoare logic prescribes that each instruction must be surrounded by two assertions. The first one describes the condition of the program state that is expected before the instruction and the second one describes the state resulting from the execution of the instruction. The precondition-postcondition pair are the assertions for the whole function. The assertions for other instructions are written in curly brackets located between instructions. To save notational burden we do not write the first and last assertions in function as these are expressed with precondition and postcondition respectively. Therefore, the initial assignments decorated with the assertions look as follows:

begin
    x := 1
    { n >= 1 /\ x = 1 }
    y := 0
    { n >= 1 /\ x = 1 /\ y = 0 }
    while x <= n do

The loop invariant condition, i.e. the formula that at the entry point to the loop at each its iteration, is marked with a special keyword invariant. So the while loop header augmented with the invariant is as follows:

while x <= n do
invariant y = x * (x-1) / 2 /\ x<= n+1 /\ n >= 1
begin

This invariant formula can be named to make future reference more accurate:

invariant gauss: y = x * (x-1) / 2 /\ x<= n+1 /\ n >= 1

Again, the presence of the invariant formula gives us excuse not to mention assertions at the beginning and at the end of loop body as they equal to the invariant. This makes the loop body look as follows:

begin
    y := y + x
    { y - x = x * (x-1) / 2 /\ x<= n /\ n >= 1 }
    x := x + 1
end

We can now combine all the assertions with the code and obtain the complete example:

function sum( n : Z ) : Z
   	precondition natural: n >= 1
   	postcondition gauss: sum = n * (n+1) / 2
   	var x : Z
   	    y : Z
begin
   	x := 1
   	{ n >= 1 /\ x = 1 }
   	y := 0
   	{ n >= 1 /\ x = 1 /\ y = 0 }
   	while x <= n do
   	invariant gauss: y = x * (x-1) / 2 /\ x<= n+1 /\ n >= 1
   	begin
     		y := y + x
     		{ y - x = x * (x-1) / 2 /\ x<= n /\ n >= 1 }
     		x := x + 1
    end
   	{ y = n * (n+1) / 2  }
   	sum := y
end