Requiem for a Bug – Verifying Software, Part 2: Formal Verification through SPARK 2014

This article is part of the Embedded Software Series: Enforced Coding Using Ada Contracts

Download this article in .PDF format

In our previous article (“Requiem for a Bug—Verifying Software: Testing and Static Analysis”), we presented a sample Ada program to perform a binary search of a sorted array, and we used both traditional testing and the CodePeer static analysis tool to locate bugs. Here’s the code that we came up with:

type Integer_Array is array (Positive range <>) of Integer;
   -- Positive is the subset of Integer values in the range 1 .. Integer'Last
   -- An object of type Integer_Array has a Positive lower bound and any upper bound 

function Search (A : Integer_Array; Value : Integer) return Natural is
   -- Natural is the subset of Integer values in the range 0 .. Integer'Last
  Left, Right, Split : Positive;
   begin
  if A'Length = 0 then
     return 0;
  end if;
  Left  := A'First;
  Right := A'Last;

  if A (Left) > Value then
     return 0;
  end if;

  while Left <= Right loop
     Split := (Left + Right) / 2;
     if A (Split) = Value then
        return Split;
     elsif A (Split) < Value then
        Left := Split + 1;
     else
        Right := Split - 1;
     end if;
  end loop;
  return 0;
   end Search;

Let's now move to formal verification using SPARK 2014 technology.¹ SPARK 2014 comprises a language (a subset of Ada 2012) and a static analysis tool that can be used to prove various program properties. Its benefits somewhat depend on how much effort you put in. You could try to just eliminate run-time errors (i.e., ensure that errors such as out-of-bounds indices don’t occur). Or, you could go for full functional verification against formally specified requirements. However, this usually requires adding contracts.

In Ada 2012 and SPARK 2014, contracts are Boolean expressions that you can attach to subprogram declarations, specifying their requirements on callers (the precondition) and their guaranteed results (the postcondition). In this example, the binary search will only work for sorted arrays (that’s the precondition), and it will either return zero if the value is not in the array, or return an index for the found value. You can express such contracts in Ada 2012 (and in SPARK 2014) as follows:

function Sorted (A : Integer_Array) return Boolean is
     (A'Length < 2 or else
  (for all X in A'First .. A'Last - 1 =>
       (for all Y in X + 1 .. A'Last => A (X) <= A (Y))));

   function Search (A : Integer_Array; Value : Integer) return Natural
     with Pre => Sorted (A),
      Post =>
       (if Search'Result = 0 then
      (for all Index in A'Range => A (Index) /= Value)
        else
          A (Search'Result) = Value));

We first introduced a Boolean function “Sorted,” which returns True if its argument is sorted. Note the use of Ada 2012 quantified expressions. Then we restrict the application of our Search function to sorted arrays by putting the expression Sorted(A) in the precondition. Finally, we express in the postcondition what we expect from the function result: If it returns 0, then Value is not in the array, and if it returns some other number, then this is an index into the array whereby the array element at this index contains Value.

We can be alerted to some problems by running the SPARK tool on our code alerts. It identifies three possible run-time errors, and indicates that it can’t establish the postcondition. Let’s look at these issues one by one.

The first possible run-time error is in this line:

Split := (Left + Right) / 2;

Clearly the addition can overflow, namely when we have a large array and are searching close to the right. This exact same bug has been found in other implementations of binary search.²

Actually, in Ada, this problem can come up even with small arrays. That’s because the first index of the array in Ada may be some large positive number close to the largest representable integer. Therefore, we need to avoid that overflow, which means writing the computation of the split point a bit differently:

Split := Left + (Right - Left) / 2;

Again, not surprisingly, we didn't find this by testing; we should have tested with very large arrays. With its default settings, which attempt to minimize “false alarms,” CodePeer didn’t report the potential overflow. Under a different set of options for the tool, the problem would have been detected.

The next possible runtime error is the following line:

if A (Split) = Value then

Here SPARK complains that Split may not be in the range of the array. However, because Left and Right are in the range of the array, Split clearly is in the range, too.

This, in fact, is a false alarm of the SPARK tool. The problem is that at that point, SPARK can't figure out the possible range of these variables alone, particularly because they’re modified in the loop. In fact, one needs to explain to SPARK what happens to the variables that are modified in the loop. You can do that using pragma Loop_Invariant. Here, the interesting property is that Left and Right always stay within the array bounds:

while Left <= Right loop
     pragma Loop_Invariant (Left  in A'Range);
     pragma Loop_Invariant (Right in A'Range);
     ...

This eliminates the error message about Split. Again, it was not a real error, but a case where the user didn’t provide enough information to make SPARK realize that the problem could never occur.

The last run-time error reported by SPARK is a possible overflow on the addition here:

elsif A (Split) < Value then
        Left := Split + 1;

How can Split become so large that adding one will make it overflow? This can occur when A'Last is close to the maximal integer value; for example, with very large arrays, or, as with the overflow above, even with small arrays in Ada when the lower bound is large. Still, shouldn't Left stay within the array bounds anyway? In fact, this bug is very similar to the very first one we found using testing. We need to protect against the case where the value we’re looking up is greater than the largest (rightmost) value in the array.

To fix this, we add the following test before the while loop:

if A (Right) < Value then
     return 0;
  end if;

This makes our code free of run-time errors! But does it always return a correct result? SPARK still complains about the postcondition.

Once again, a situation arises where we need to help SPARK by telling it which property is maintained. In this case, it’s actually very simple: We just have to indicate the zone of the array that we’re searching in. In other words, we need to indicate the zones of the arrays we’ve already excluded. We express this property through pragma Loop_Invariant:

pragma Loop_Invariant
    (for all Index in A'Range =>
        (if Index < Left or Index > Right then A (Index) /= Value));

SPARK can now prove the entire code correct—free of run-time errors and fully functionally correct (i.e., its postcondition will be true if its precondition is satisfied).

Here is the final implementation:

function Search (A : Integer_Array; Value : Integer) return Natural is
  Left, Right, Split : Positive;
   begin
  if A'Length = 0 then
     return 0;
  end if;
  Left  := A'First;
  Right := A'Last;

  if A (Left) > Value then
     return 0;
  end if;
  if A (Right) < Value then
     return 0;
  end if;
  while Left <= Right loop
     pragma Loop_Invariant (Left  in A'Range);
     pragma Loop_Invariant (Right in A'Range);
     -- Value is not before left and not after right
     pragma Loop_Invariant
       (for all Index in A'Range =>
       (if Index < Left or Index > Right then A (Index) /= Value));
     Split := Left + (Right - Left) / 2;
     if A (Split) = Value then
        return Split;
     elsif A (Split) < Value then
        Left := Split + 1;
     else
        Right := Split - 1;
     end if;
  end loop;
  return 0;
   end Search;

Summary

How did the different verification methods fare in my comparison? First of all, my initial implementation wasn't too bad—it always computed the right result, but failed to protect against some possible run-time errors. Therefore, maybe the comparison isn’t that meaningful, because no functional bugs were to be found.

Testing gave us some confidence that the program was functionally correct and it found a common run-time error (searching for a value that’s smaller than the smallest entry in the array), but missed some others (searching in an empty array and searching for a value larger than the largest element). With more extensive testing, the case of the empty array would probably have been found.

CodePeer is very easy to run; much easier than writing tests. In its default settings, CodePeer uncovered a bug that’s very likely to occur, namely the empty array case. When set to maximal detection of potential errors, CodePeer would have found all run-time errors in the example.

A limitation of a static analysis tool like CodePeer is that it’s mostly useful in finding possible run-time errors. However, it generally can’t find functional errors, because CodePeer has no idea what your code is supposed to be doing. Nonetheless, it will point out many suspicious situations that may impact functional correctness. This was not the case in my example, though. That said, static analysis is very easy to apply, so it should always be part of your verification activities. You can control the tradeoff between maximal detection of potential errors and minimal reporting of “false alarms.”

Finally, formal verification (e.g., using SPARK) can be used in a similar fashion to static analysis to find all run-time errors in your code, even the most unlikely of errors that may go undetected for years, such as the numerical overflow in the computation of Split. In addition, formal verification can tell you whether your code is functionally correct in all situations. This is where formal verification (SPARK) provides more power than static analysis (CodePeer), because expressing functional correctness usually requires complex assertions (like the for all expressions in our example) that are too complex for static-analysis tools to use.

However, formal verification requires more effort, because you need to include a formal specification of the program’s requirements (e.g., through contracts). Depending on your application, this effort may be overkill (e.g., a utility program that’s only used internally) or on the contrary, may be essential to the safety or security of your users.

Read more from the Embedded Software Series: Enforced Coding Using Ada Contracts

Download this article in .PDF format