Examples

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

Cubic root

axiom cubicbin: forall b : Z, (b + 1) ^ 3 = b ^ 3 + 3 * (b ^ 2) + 3 * b + 1 
axiom squarebin: forall b : Z, (b + 1) ^ 2 = b ^ 2 + 2 * b + 1

function croot( x : Z ) : Z
	precondition x >= 0
	postcondition (croot-1)^3 <=  x /\ x < croot^3
	var a : Z
		b : Z
		y : Z
begin
	a := 1
	{ x >= 0 /\ a = 1 }
	b := 1
	{ x >= 0 /\ a = 1 /\ b = 1 }
	y := 1
	{ x >= 0 /\ a = 1 /\ b = 1 /\ y = 1}
	while y <= x do
	invariant (b-1)^3 <=  x /\  y = b^3 /\ a = b ^ 2 /\ x >= 0
	begin
  		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
  		{ (b ^ 3) <=  x /\ y = (b +1) ^ 3 /\ 
  		  a = (b+1)^2 /\ x >= 0 }
  		b := b + 1
  	end
	{ (b-1) ^ 3 <=  x /\ x < b ^3 }
	croot := b
end

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

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

axiom tozero: forall z : Z p : Z, z * (p ^ 0) = z
axiom odddiv2: forall z : Z p : Z q : Z, 
  odd(q) -> z * p ^ q = z * p ^ (2 * (q / 2) + 1)
axiom twoinexp: forall z : Z p : Z q : Z, z * p ^ (2 * q) = z * (p * p ) ^ q
axiom twoandoneinexp: forall z : Z p : Z q : Z, 
  z * (p ^ ((2 * q) + 1)) = z * ((p * p) ^ q) * p

function power( y : Z, x : Z ) : Z 
  precondition n_ge_one : y >= 0
  precondition xnz : x <> 0
  postcondition power = x ^ y
  var z : Z
      p : Z
      q : Z
begin
  z := 1
  { p = p /\ z = 1 /\ y >= 0 /\ x <> 0 }
  p := x
  { q = q /\ p = x /\ z = 1 /\ y >= 0 /\ p <> 0 }
  q := y
  { q = y /\ p = x /\ z = 1 /\ y >= 0 /\ p <> 0 }
  while q <> 0 do
  invariant z * p ^ q = x ^ y /\ q >= 0 /\ y >= 0 /\ p <> 0
  begin
      if q mod 2 = 1 then
          begin
        z := z * p
      end
      { (odd(q) /\ q = 2 * (q / 2) + 1 /\ (z * p ^ q = (x ^ y) * p ))
        \/ 
        (not odd(q) /\ (z * p ^ (2 * (q / 2)) = x ^ y)) }
      { q > 0 }
      { y >= 0 }
      { p <> 0 }
      q := q / 2
      { z * (p * p) ^ q = x ^ y }
      { q >= 0 }
      { y >= 0 }
      { p <> 0 }
      p := p * p
    end
    { z * (p ^ q) = x ^ y /\ q = 0 /\ y >= 0 }
    power := z
end

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.

Binary search

predicate ordered(A : ARRAY [Z], i : Z, j : Z) = forall x : Z y : Z,
    i <= x -> x <= y -> y <= j -> A[x] <= A[y]
predicate is_in(A : ARRAY [Z], v : Z, i : Z, j : Z) = exists x : Z,
    (i <= x /\ x <= j) /\ A[x] = v

function bsearch( A : ARRAY [Z], len : Z , v : Z ) : Z 
  precondition n_ge_one : len >= 1 //lenght ia st least 1
  precondition orderedA: ordered(A, 1, len)//array is ordered
  precondition is_inA: is_in(A, v, 1, len) //the value we look for is in the array
  postcondition A[bsearch] = v //the result is a pointer to the value we look for 
  var i : Z
      j : Z
      k : Z
begin
  i := 1
  { i = 1 /\ len >= 1 /\ ordered(A, 1, len) /\ is_in(A, v, 1, len) }
  j := len
  { i = 1 /\ j = len /\ len >= 1 /\ ordered(A, 1, len) /\ is_in(A, v, 1, len) }
  while i < j do
    invariant is_in(A, v, i, j) /\ ordered(A, i, j) /\ i<=j
  begin
      k := (i + j) / 2
      { is_in(A, v, i, j) /\ ordered(A, i, j) /\ i<j /\ k = (i+j)/2 }
      if A[k] < v then
        i := k + 1
      else
        j := k
    end
    { is_in(A, v, i, i) }
    bsearch := i
end

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.

Quicksort partition

predicate left_contains_le (A : ARRAY[Z], where : Z, val : Z) =
  forall i : Z , (1 <= i /\ i < where) -> A[i] <= val

predicate right_contains_gt (A : ARRAY[Z], where : Z, bound : Z, val : Z) =
  forall i : Z, (where < i /\ i <= bound) -> A[i] > val
  
predicate sides_parted(A : ARRAY[Z], left : Z, right :Z, bound : Z, val : Z) =
  left_contains_le(A, left, val) /\ right_contains_gt(A, right, bound, val)

predicate is_copy(A : ARRAY[Z], B : ARRAY[Z], len : Z) =
  forall i : Z, (1 <= i /\ i <= len) -> A[i] = B[i]
 
predicate between(l : Z, m : Z, r : Z) = l <= m /\ m <= r


function partition(A : ARRAY[Z], len : Z) : ARRAY[Z]
  precondition  1 <= len
  postcondition
    exists k : Z, sides_parted(partition, k, k, len, A[1])
  var v : Z
      i : Z
      j : Z
      x : Z
begin
  partition := A
  { is_copy(A, partition, len) /\ 1 <= len }
  v := A[1]
  { is_copy(A, partition, len) /\ 1 <= len /\ v = partition[1] /\ v = A[1] }
  partition[len+1] := v + 1
  { is_copy(A, partition, len) /\ 1 <= len /\ v = partition[1] /\ v = A[1] /\
    partition[len+1] > v
  }
  i := 2 
  { is_copy(A, partition, len) /\ 1 <= len /\ v = partition[1] /\ v = A[1] /\
    partition[len+1] > v /\ i = 2
  }
  j := len
  { is_copy(A, partition, len) /\ 1 <= len /\ v = partition[1] /\ v = A[1] /\
    partition[len+1] > v /\ i = 2 /\ j = len
  }
  x := 0
  { is_copy(A, partition, len) /\ 1 <= len /\ v = partition[1] /\ v = A[1] /\
    sides_parted(partition, i, j, len, v) /\
    partition[len+1] > v /\ i = 2 /\ j = len /\ x = 0
  }
  while i <= j do 
    invariant pointers: j + 1 >= i - 1 /\ between(2, i, len+1) /\ between(1, j, len)
    invariant sides: sides_parted(partition, i, j, len, v)
    invariant guards: partition[1] = v /\ partition[len+1] > v
    invariant general: 1 <= len /\ v = A[1]
  begin
    while partition[i] <= v do
      invariant pointers: j+1 >= i - 1 /\ between(2, i, len+1) /\ between(1, j, len)
      invariant sides: sides_parted(partition, i, j, len, v) 
      invariant guards: partition[1] = v /\ partition[len+1] > v
      invariant general: 1 <= len /\ v = A[1]
    begin
      i := i + 1
    end
    { j+1 >= i - 1 /\ between(2, i, len+1) /\ between(1, j, len) /\
      sides_parted(partition, i, j, len, v) /\ 
      partition[1] = v /\ partition[len+1] > v /\ partition[i] > v /\
      1 <= len /\ v = A[1] }
    while partition[j] > v do
      invariant pointers: j + 1 >= i - 1 /\ between(2, i, len+1) /\ between(1, j, len)
      invariant sides: sides_parted(partition, i, j, len, v)  
      invariant guards: partition[1] = v /\ partition[len+1] > v /\ partition[i] > v
      invariant general: 1 <= len /\ v = A[1]
    begin
      j := j - 1
    end
    { j + 1 >= i - 1 /\ between(2, i, len+1) /\ between(1, j, len) /\
      sides_parted(partition, i, j, len, v) /\  
      partition[1] = v /\ partition[len+1] > v /\ partition[i] > v /\ partition[j] <= v /\
      1 <= len /\ v = A[1] }
    if i < j then 
    begin
      x := partition[i]
      { 1 < i /\ i < j /\ between(2, i, len+1) /\ between(1, j, len) /\
        sides_parted(partition, i, j, len, v) /\  
        partition[1] = v /\ partition[len+1] > v /\ partition[j] <= v /\ 
        x = partition[i] /\ x > v /\
        1 <= len /\ v = A[1] }
      partition[i] := partition[j]
      { 1 < i /\ i < j /\ between(2, i, len+1) /\ between(1, j, len) /\
        sides_parted(partition, i + 1, j, len, v) /\  
        partition[1] = v /\ partition[len+1] > v /\ partition[j] <= v /\ 
        x > v /\
        1 <= len /\ v = A[1] }
      partition[j] := x
      { 1 < i /\ i < j /\ between(2, i, len+1) /\ between(1, j, len) /\
        sides_parted(partition, i + 1, j - 1, len, v) /\  
        partition[1] = v /\ partition[len+1] > v /\ 
        x > v /\ 1 <= len /\ v = A[1] }
      i := i + 1
      { 1 < i /\ i < j + 1 /\ between(2, i, len+1) /\ between(1, j, len) /\
        sides_parted(partition, i, j - 1, len, v) /\  
        partition[1] = v /\ partition[len+1] > v /\  
        x > v /\
        1 <= len /\ v = A[1] }
      j := j - 1
    end
  end
  { i > j /\ j + 1 >= i - 1 /\ between(2, i, len+1) /\ between(1, j, len) /\
    sides_parted(partition, i, j, len, v) /\
    partition[1] = v /\ partition[len+1] > v /\
    1 <= len  /\ v = A[1] }
  partition[1] := partition[j]
  { i > j /\ j + 1 >= i - 1 /\ between(2, i, len+1) /\ between(1, j, len) /\
    sides_parted(partition, i, j, len, v) /\
    partition[len+1] > v /\
    1 <= len  /\ v = A[1] }
  partition[j] := v
end

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.