Here is a number of examples that illustrate a few specific features of the HAHA language.
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.
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.
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.
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.