Proving the correctness of a binary search procedure with SPARK/Ada
Introduction
SPARK/Ada is a language derived from Ada that allows for a formal checking (i.e., mathematically prove the correctness) of the software. Several types of checks can be done: from the absence of runtime exceptions to no use of uninitialized variables, up to the formal proof that a given procedure/function fulfills its contract.
I like formal checking because it can actually prove that your program is correct (or that, at least, some kind of errors are absent), something that is usually not possible with testing. Of course, formal checking cannot applied to every program, but when it is possible it is a very powerful tool.
SPARK/Ada is definitively on my list of stuff that I want to learn.
Recently I had to write a procedure for a binary search in an ordered array. I thought that it could be an interesting exercise to write it in SPARK/Ada in order to have it formally verified. This is a brief summary of this experience, written with a tutorial spirit.
The requirements
The problem I want to solve is the following

INPUTS

Table
: an array ofFloat
sorted in strictly increasing order (that is,Table(n+1) > Table(n)
for everyn
). 
What
: aFloat
such that it is included between the array extremes, that is,
Table(Table'First) โค What โค Table(Table'Last)
, but  it is not necessarily in
Table
, that is it is not required that there isn
such thatTable(n) = What
 it is included between the array extremes, that is,


OUTPUTS
 The unique index
n
such that
 The unique index
Table(n) โค What < Table(n+1)
The solution
The spec file
First basic draft of specs
Let's first flesh out the spec file (roughly [very roughly] similar to a *.h
file for you C people).
pragma SPARK_Mode (On);
package Searching is
subtype Element_Type is Float;
subtype Index_Type is Natural;
type Array_Type is
array (Index_Type range <>) of Element_Type;
function Find (What : Element_Type;
Table : Array_Type)
return Index_Type;
end Searching;
Entering SPARK Mode
The first line we encounter is
pragma SPARK_Mode (On);
This claims that this package will be compatible with SPARK restrictions and conventions. The lines
subtype Element_Type is Float;
subtype Index_Type is Natural;
define Element_Type
and Index_Type
as synominous of Float
and Index_Type
, respectively. This is not strictly necessary, but it can make it easier to change the types in a future
Function declaration
function Find (What : Element_Type;
Table : Array_Type)
return Index_Type;
should be clear enough.
Introducing contracts
In order for SPARK to be able to proof that our implementation of Find
is correct, we need to describe to SPARK what we expect Find
to do. This is done by means of a contract. Like a normal contract between people, a function contract usually has two parts: preconditions and postconditions.
The idea is that if you (the caller) do your part (i.e. you meet the preconditions when you call me), then I, the function, promise to do my part, that is, that the result will satisfy the postconditions.
If a contract is given, I can ask SPARK to prove that the postconditions follow from the preconditions. If SPARK succeeds, I know that the code I wrote is correct (in the sense that it respects the contract) without doing any test: I have a mathematical proof for it.
BTW, contracts are very useful even if you are not using SPARK. First, they are a wonderful "bug trap." By using the right options, you can ask the compiler to insert code that checks the preconditions when the function is called and the postconditions when the function ends. If pre/postconditions are not met, an exception is raised.
Moreover, contracts document in a formal and unambiguous way the behavior of the function and, differently from usual commentbased documentation, cannot go out of sync with the code.
OK, so contracts are cool. How do we write the contract for our function? Well, let's start with the precondition and let's check the specs. It is said that (i) Table
must be sorted and (ii) What
must be between Table
extrema; we just translate that in Ada in this way
function Find (What : Element_Type;
Table : Array_Type)
return Index_Type
with
Pre =>
Is_Sorted (Table)
and Table (Table'Last) >= What
and What >= Table (Table'First);
where Is_Sorted
is a function that checks if its argument is sorted and defined as follows
function Is_Sorted (Table : Array_Type) return Boolean
is (for all L in Table'Range =>
(for all M in Table'Range =>
(if L > M then Table (L) > Table (M))))
with Ghost;
The body of the function (this form is called expression function) is the translation in Ada of the definition of monotonic array.
Note the
with Ghost
in the definition. This says thatIs_Sorted
is a ghost function, that is, a function that can be used only in contracts or assertions; if used in other places ("real code") an error is raised. (I love this kind of protections โฅ)
The preconditions look right and they represent the actual specs, but if we try to run SPARK we get an error
medium: array index check might fail
at line
and What >= Table (Table'First);
This means that Table'First
, that is the first index of the array, can be ... outside array bounds? The first index is by definition within the bounds, right?
Go home SPARK, you're drunk...
Well... Actually, SPARK is right. If you ask for a counterexample you get
e.g. when Table'First=1 and Table'Last=0
Now, when in the world can be possible that the last index is smaller than the first one?!? Well, if Table
is empty... Empty arrays in Ada have the last index smaller than the first one. Therefore, trying to access Table (Table'First)
would cause an error.
Well, SPARK, good catch...
Well, I agree (although it could happen because of an error), but SPARK does not know it. To make SPARK happy it suffices to add Table'Length > 0
to the precondition to get
function Find (What : Element_Type;
Table : Array_Type)
return Index_Type
with
Pre => Table'Length > 0
and then (Is_Sorted (Table)
and Table (Table'Last) >= What
and What >= Table (Table'First));
Now SPARK is happy and even the casual user sees that you cannot call the function with an empty table.
The postcondition
Also for the postconditions we translate directly the requirement from English to Ada. It is required that What
is between Table(n)
and Table(n+1)
where n
is the value returned by the function. In Ada we get
(if Find'Result = Table'Last then
Table (Find'Result) = What
else
Table (Find'Result) <= What
and What < Table (Find'Result + 1));
Note that Find'Result
is the value returned by Find
and that we consider as special case Find'Result = Table'Last
since in this case there is no "following entry" in Table
. Overall, the function declaration with the full contract is
function Find (What : Element_Type;
Table : Array_Type)
return Index_Type
with
Pre =>
Table'Length > 0
and then (Is_Sorted (Table)
and Table (Table'Last) >= What
and What >= Table (Table'First)),
Post =>
(if Find'Result = Table'Last then
Table (Find'Result) = What
else
Table (Find'Result) <= What
and What < Table (Find'Result + 1));
The body file (implementation)
The algorithm
The algorithm for a binary search is well known and exemplified in the following picture
Basically, we keep two "cursors" in the table: Bottom
and Top
with the condition that it must always be
Table(Bottom) โค What < Top(top)
We get the Middle
point between Top
and Bottom
and if Table(Middle)
is too large we move Top
to Middle
, otherwise we move Bottom
. We iterate this until on of the following two conditions holds

Table(Bottom) = What
, that is, we actually foundWhat
inTable

Top = Bottom+1
there are no intermediate entries betweenTop
andBottom
In both cases we return Bottom
The actual code
Let's start with a basic skeleton of the procedure.
function Find (What : Element_Type; Table : Array_Type) return Index_Type
is
Bottom : Index_Type;
Top : Index_Type;
Middle : Index_Type;
begin
if Table (Table'Last) = What then
return Table'Last;
end if;
Bottom := Table'First;
Top := Table'Last;
pragma Assert (Table (Top) > What and What >= Table(Bottom));
while Table (Bottom) < What and Top  Bottom > 1 loop
Middle := (Bottom + Top)/2;
if Table (Middle) > What then
Top := Middle;
else
Bottom := Middle;
end if;
end loop;
return Bottom;
end Find;
It is just a translation of the algorithm informally described above. Note how the special case Table (Table'Last) = What
is handled separately; in this way we know that
Table (Top) > What and What >= Table(Bottom)
holds (see the pragma Assert
).
Now, in order to make it easier for SPARK to prove the correctness of the code we insert in the code some pragma Assert
claiming properties that hold true in different points of the code.
Automatic theorem proving is not easy and some hint to the prover can help. Moreover, I love spreading generously my code with assertion since they help understanding what the code does and which properties I expect to be true. They are also formidable "bug traps".
The function body with all the assertions looks like
function Find (What : Element_Type; Table : Array_Type) return Index_Type
is
Bottom : Index_Type;
Top : Index_Type;
Middle : Index_Type;
begin
if Table (Table'Last) = What then
return Table'Last;
end if;
pragma Assert (Table (Table'Last) > What);
Bottom := Table'First;
Top := Table'Last;
pragma Assert (Bottom < Top);
pragma Assert (Table (Bottom) <= What and What < Table (Top));
while Table (Bottom) < What and Top  Bottom > 1 loop
pragma Loop_Invariant (Bottom >= Table'First);
pragma Loop_Invariant (Top <= Table'Last);
pragma Loop_Invariant (Top > Bottom);
pragma Loop_Invariant (Table (Bottom) <= What and What < Table (Top));
pragma Loop_Variant (Decreases => Top  Bottom);
Middle := (Bottom + Top)/2;
pragma Assert (Bottom < Middle and Middle < Top);
if Table (Middle) > What then
Top := Middle;
else
Bottom := Middle;
end if;
end loop;
pragma Assert (Table (Bottom) <= What and Table (Bottom + 1) > What);
return Bottom;
end Find;
There are just two points worth describing; the first is this sequence of pragma
s inside the loop
pragma Loop_Invariant (Bottom >= Table'First);
pragma Loop_Invariant (Top <= Table'Last);
pragma Loop_Invariant (Top > Bottom);
pragma Loop_Invariant (Table (Bottom) <= What
and What < Table (Top));
pragma Loop_Variant (Decreases => Top  Bottom);
pragma
s Loop_Invariant
and Loop_Variant
are specific to SPARK. A loop invariant is a condition that is true at every iteration and you can see that this loop invariant is a formalization of what we said before: at every iteration What
is between Top
and Bottom
. Loop invariants are important in the proof of correctness of while
loops.
A while
loop can potentially go on forever; a technique that allows us to prove that the loop will terminate is to search for some value that always increases (or decreases) at every iteration; if we know a bound for this value (e.g., it is always positive and it always decreases) we can deduce that the loop will terminate. The pragma
Loop_Variant
allows us to declare said value. In this case the distance between Top
and Bottom
is halved at every iteration, therefore it is a good variant. Since TopBottom
cannot be smaller than 2 (see condition in the while), we deduce that the loop will terminate.
A second observation is about seemly innocuous line
Middle := (Top + Bottom) / 2;
Here SPARK complains with
medium: overflow check might fail
(e.g. when Bottom = Index_Type'Last4 and Top = Index_Type'Last2)
Good catch! Here SPARK is observing that although theoretically Middle
should be in the range of representable integers if Top
and Bottom
are, there is a possibility of an overflow while doing the sum. Since on my PC Index_Type'Last = 2^631
, it is unlikely that one would work with tables so big, nevertheless...
We have two solutions: (i) allow a smaller range of integers (that is, up to Index_Type'Last/2
) or (ii) compute the mean with function
function Mean (Lo, Hi : Index_Type) return Index_Type
is (Lo + (Hi  Lo) / 2)
with
Pre => Lo < Index_Type'Last and then Hi > Lo + 1,
Post => Hi > Mean'Result and Mean'Result > Lo;
that is guaranteed to have no overflow. Note that in the precondition we require that Hi > Lo + 1
, this is guaranteed by the loop condition and it is necessary in order to guarantee that the post conditions hold which in turn guarantees that the loop variant decreases at every iteration.
Finally...
OK, now if we run SPARK we get
Summary of SPARK analysis
=========================

SPARK Analysis results Total Flow Interval CodePeer Provers Justified Unproved

Data Dependencies . . . . . . .
Flow Dependencies . . . . . . .
Initialization 3 3 . . . . .
NonAliasing . . . . . . .
Runtime Checks 29 . . . 29 (CVC4) . .
Assertions 14 . . . 14 (CVC4) . .
Functional Contracts 3 . . . 3 (CVC4) . .
LSP Verification . . . . . . .

Total 49 3 (6%) . . 46 (94%) . .
Do you see on the extreme right the column Unproved
with no entries? That is what I want to see... SPARK was able to prove everything, so now you can kick back, relax and enjoy your binary search function with confidence: you made terra bruciata (scorched earth) around it and no bug can survive.