Introduction

A loop invariant is a property that holds true before each iteration of a loop and after the loop terminates. For linear search, the loop invariant is: "the target element is not in the portion of the array already examined." This property is used to formally prove that the algorithm is correct — it finds the target if it exists and correctly reports absence if it does not. Understanding loop invariants is fundamental to algorithm analysis and is commonly tested in computer science courses and interviews.

Linear Search Algorithm

1def linear_search(arr, target):
2    for i in range(len(arr)):
3        if arr[i] == target:
4            return i
5    return -1

The algorithm checks each element sequentially. If it finds the target, it returns the index. If it exhausts the array, it returns -1.

The Loop Invariant

Statement: At the start of iteration i, the target is not present in arr[0..i-1].

The three parts of a loop invariant proof:

Initialization (Before the First Iteration)

Before the loop starts, i = 0. The subarray arr[0..-1] is empty. The target is trivially not in an empty subarray. The invariant holds.

Maintenance (Each Iteration Preserves the Invariant)

Assume the invariant holds at the start of iteration i: the target is not in arr[0..i-1]. During iteration i:

• If arr[i] == target, the function returns i — the loop terminates with the correct answer
• If arr[i] != target, the target is not in arr[0..i]. At the start of the next iteration (i+1), the invariant holds for arr[0..i]

Termination (After the Loop Ends)

The loop ends when i == len(arr). By the invariant, the target is not in arr[0..len(arr)-1], which is the entire array. Returning -1 is correct.

Formal Pseudocode with Invariant

1LinearSearch(A, n, target):
2    // Invariant: target is not in A[0..i-1]
3    for i = 0 to n-1:
4        // Invariant holds: target not in A[0..i-1]
5        if A[i] == target:
6            return i   // Found at index i
7        // Now: target not in A[0..i]
8    // Invariant: target not in A[0..n-1] (entire array)
9    return -1          // Not found

Python Implementation with Assertions

1def linear_search_verified(arr, target):
2    n = len(arr)
3    for i in range(n):
4        # Loop invariant: target not in arr[0:i]
5        assert target not in arr[0:i], f"Invariant violated at i={i}"
6
7        if arr[i] == target:
8            return i
9
10    # Post-condition: target not in arr[0:n] (entire array)
11    assert target not in arr
12    return -1
13
14# Test
15print(linear_search_verified([3, 7, 1, 9, 4], 9))   # 3
16print(linear_search_verified([3, 7, 1, 9, 4], 5))   # -1

The assertions verify the invariant at each step. In production code, remove them — they serve as a proof aid.

Comparing with Binary Search Invariant

Linear search and binary search have different loop invariants:

1def binary_search(arr, target):
2    """
3    Loop invariant: if target is in arr, then target is in arr[lo..hi]
4    """
5    lo, hi = 0, len(arr) - 1
6    while lo <= hi:
7        # Invariant: if target in arr, then target in arr[lo..hi]
8        mid = (lo + hi) // 2
9        if arr[mid] == target:
10            return mid
11        elif arr[mid] < target:
12            lo = mid + 1
13        else:
14            hi = mid - 1
15    return -1

Loop Invariants for Other Algorithms

Loop invariants are used to prove correctness of many algorithms:

1# Insertion sort invariant: arr[0..i-1] is sorted
2def insertion_sort(arr):
3    for i in range(1, len(arr)):
4        # Invariant: arr[0:i] is sorted
5        key = arr[i]
6        j = i - 1
7        while j >= 0 and arr[j] > key:
8            arr[j + 1] = arr[j]
9            j -= 1
10        arr[j + 1] = key
11    # Post-condition: arr[0:n] is sorted
12    return arr
13
14# Selection sort invariant: arr[0..i-1] contains the i smallest
15# elements in sorted order

Common Pitfalls

• Confusing the invariant with the termination condition: The loop invariant describes what is true throughout the loop, not when the loop stops. The termination condition (i == n) combined with the invariant proves the post-condition.
• Not checking all three parts: A valid loop invariant proof requires initialization, maintenance, and termination. Skipping any part leaves the proof incomplete and may hide bugs.
• Choosing a trivially true invariant: "True" is a valid invariant but proves nothing about correctness. The invariant must be strong enough to imply the post-condition when combined with the loop termination condition.
• Forgetting the early return case: In linear search, the loop may terminate early via return i. The invariant proof for maintenance must handle both the "found" case (early return) and the "not found" case (loop continues).
• Off-by-one in the invariant range: The invariant says target is not in arr[0..i-1], not arr[0..i]. At the start of iteration i, element arr[i] has not been checked yet. Getting this boundary wrong invalidates the proof.

Summary

• The linear search loop invariant is: "the target is not in arr[0..i-1]" at the start of iteration i
• Prove correctness via three steps: initialization (true before loop), maintenance (preserved each iteration), termination (implies correct result)
• The invariant combined with the termination condition (i == n) proves that returning -1 is correct
• Loop invariants are the standard technique for formally proving algorithm correctness
• Linear search invariant narrows the unsearched space by one element per iteration; binary search narrows by half
• Practice identifying invariants for insertion sort, selection sort, and binary search to build intuition