Loop Invariant Linear Search

Linear Search

Hello! This is part 6 in a series of short articles on loop invariants. You can refer to the first part (introduction) here. Today, we are going to develop an algorithm for linear search using loop invariants. Let us get started.

Problem definition

Given an array (A) containing (n) numbers and given some value (v). If (v) is found in (A) then the array index (i) that corresponds to (v) should be returned otherwise if (v) is not found in (A) then (-1) is returned. As we can see, this problem is very easy to solve. We just need to scan the array looking for (v), once we find it we return its index, otherwise we continue scanning the array until all elements in the array are checked. If we do not find (v) in (A) we return (-1) which means element is not found. Since the problem is very easy to solve, one can quickly write the code using intuition however we are going to use loop invariants instead.

Identify the goal of the loop and write it as a post condition

The goal of the algorithm is to find the index of the first element in (A) that is equal to (v) otherwise if there is no such element then the result should be (-1). Here is our suggested post condition:

Write the loop specifying the guard (loop condition)

We will be using a while loop in our demonstration because it clearly separates the guard (loop condition) from initialization and loop index, however we can use any other kind of loop if we wish (for example a for loop). Here is the skeleton of the while loop along with the post condition from step 1:

Fill in the loop invariant

Loop invariant should describe the goal of the algorithm. It should hold true just before entering the loop and after each iteration. It should give an idea about the current progress towards the final goal. Let us use the following loop invariant: “(v) is not found in the first (k – 1) elements”. The fact that (v) is not found yet in the first (k – 1) tells us about the current progress of the algorithm. It is either going to find it at some (k) or even check all elements in the array without finding (v). Also, pay attention to the fact that the invariant is somehow related to the loop guard. Whenever (k > n) the loop terminates and the post condition is “(-1) should be returned”. In the next step we will set the required initialization that would make the invariant hold true before the loop and after each iteration.

Fix the initialization so that the loop invariant evaluate to true

The value (v) is initially (just before entering the loop) assumed as not found simply because no elements have been examined yet. The array index starts at (1) so the value of (k – 1) should be (0) which means we should initialize (k = 1). Let us now see how the invariant holds true just before entering the loop.

In order for the invariant to hold true after each iteration let us consider the first iteration when (k) is incremented from (1) to (2):

The last statement means the first item has been checked but it is not equal to (v). This is obviously true because otherwise if the element was found then its index should have been returned (we gonna add the if statement that checks for that before incrementing the loop index (k) in the next step)

Figure out how to achieve the goal by filling in the body of the loop

The code to check if (v) is found at some (k) position in the array is simply a comparison statement as indicated in the code below. We all know how to do comparison but that is not the main point here. We have to put the comparison statement before incrementing the loop index (k) and the reason why we do so is totally dependent on the invariant we have chosen. If we need to put the comparison statement after we increment the loop index (k) then we need do the following:

1. Change the loop invariant to “(v) is not found in the first (k) elements”
2. Initialize (k) as (k = 0)
3. Change the guard from (k <= n) to (k < n)

and this is nothing but another solution to the same problem because we just used another valid loop invariant. I will keep it to the reader to verify that the invariant “(v) is not found in the first (k) elements” holds true at initialization, after each iteration and at termination as well. Here is the final code of the algorithm:

So far we proved that our loop invariant holds true before entering the loop and maintains that after each iteration. The last step is to prove that it also holds true after the loop terminates. If the loop terminates before (v) is found and returned then (k) has to be (n + 1) so the invariant becomes

which means (v) is not found in the entire array so a (-1) is returned (this is the post condition) otherwise if it is found then the index of (v) should have been already returned earlier. That is it for today, in the next article we will discuss a new example “Bubble Sort“. Thanks for reading.