Requiem for a Bug – Software Verification: Testing and Static Analysis

This article is part of the embedded software series: Forced Coding Using Ada Contracts

Download this article in .PDF format

What are you doing to make your code behave as expected? And are the methods you have chosen as effective in finding the problems as you thought? In this article, the first of a two-part series, I will write a piece of code in Ada and then try to find bugs with two different methods:

• Test by writing a simple unit test

• Static analysis using the CodePeer tool

These approaches address the problem of software verification at increasing levels of sophistication. Although the chosen example is small, it will show what is feasible and what is not with the different verification techniques.

The sample program that will illustrate the different methods is a binary search for a particular value in a sorted array; the search function returns the index of the value (if present) and zero otherwise. The same value may appear multiple times in the array; in such a situation, the search function should return the index of a match.

Binary search is a well-known algorithm for locating a given value in a sorted array. Instead of searching the whole array from the beginning, a binary search will compare the array value in the middle of the array with the given value. If the first is higher, the search will continue to the left of this median value; otherwise, it will continue to the right. In this way, the binary search will split the search space in half on each iteration, until it finds the value or concludes that it cannot be in the array. A standard linear search has O(n) execution time, while a binary search is O(Newspaper₂(not))

Binary search is a very basic algorithm, but it’s surprisingly easy to make mistakes when programming it. This has been pointed out by great minds such as Donald Knuth¹ and Jon Bentley². If you want more information, I invite you to read a recent discussion on “Stack Overflow”³but only after reading my articles.

Here is my first attempt at implementing the binary search algorithm:

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  : Positive := A'First; -- Index of lower bound
  Right : Positive := A’Last;  -- Index of upper bound
  Split : Positive;
   begin
  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;

This implementation assumes that array indices are positive numbers (but not necessarily starting at 1). However, the result of the function is a natural value, which includes zero. This allows the function to return the special value zero, which cannot be a valid index into the array, to indicate that the value was not found.

The algorithm maintains two indices—left and right. These indicate the area in which the algorithm is currently searching. Anything outside this range has been excluded. At each step, the algorithm calculates the midpoint between Left and Right, compares the value at this index with the given value, and either returns the result or excludes the left or right area from the area to be searched. Once the area to be searched becomes empty (loop exit condition), the algorithm can return zero, indicating that the value is not there.

Sounds reasonable, right? We will first try to test to see if there are any problems. I tested this function in the following way, which seemed quite exhaustive to me:

I created an array of 10 random integers between 1 and 100, sorted in ascending order. Then I used the Search function above with this array as the first parameter, and all integers between 1 and 100 as the second parameter. For each of these values, I checked if the result was the expected one: 0 if the value is not in the array; otherwise it returns an index such that A(I)=Value.

In fact, my function crashed on the first test, with the search value 1! Why is that? I forgot to take into account the case where Value is already smaller than the first element of the array. In this case, the algorithm will set the “Right” variable to smaller and smaller values, until it attempts to set it to zero. This will eventually fail with a runtime check because Right is forced to be positive, which excludes zero.

The solution is to specifically protect against this case by adding the following check before the while loop:

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

My seemingly exhaustive test found no more issues.

Next, I ran the CodePeer static analysis tool, which examines the Ada code for potential runtime errors and logic bugs. CodePeer flags problematic constructs in source code and calculates preconditions for functions, that is, conditions that must be met by the caller. A screenshot of the CodePeer report for our example appears in the figure. In this case, it is very interesting to examine the calculated precondition for our search function:

   --    A(A'First)'Initialized
   --    A'Last >= 1
   --    A'First <= A'Last

It seems to require the array to be non-empty. And indeed my code will fail passing it an empty array (e.g. when the lower bound is 1 and the upper bound is 0). My simplistic testing strategy did not cover this case, as it was only tested with a fixed array of size 10. Fixing is very easy; we just add an appropriate test at the start of the function. Also, since Right may not be positive (i.e. when the array is empty), either its declaration must be modified or its initialization must be moved. We chose the latter, and for consistency we also moved the initialization of Left.

Here is a modified version of the program that includes fixes for the two errors we found:

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;

With its default settings, CodePeer has not identified any additional bugs in this code. Is the program now correct? We will address this issue in Part 2 of this series, when we use SPARK 2014 and formal methods to augment our verification approach.

Learn more about the embedded software series: Forced Coding Using Ada Contracts

Download this article in .PDF format

The references:

1.D.Knuth, The Art of Computer Programming, Volume 3: (2nd ed.) Sorting and Grabbingching; Addison Wesley Longman; 1998

2.J.Bentley, Pearls of Programming (Second Edition); Addison-Wesley; 2000.

3. http://stackoverflow.com/questions/504335/what-are-the-pitfalls-in-implementing-binary-search