Statement#

Consider the following binary search algorithm:

def binary_search(arr, target):
    low, high = 0, len(arr) - 1
    while low <= high:
        mid = (low + high) // 2
        if arr[mid] == target:
            return mid
        elif arr[mid] < target:
            low = mid + 1
        else:
            high = mid - 1
    return -1

Prove the correctness of this algorithm using the loop invariant technique. Your proof should include:

1. Initialization: The invariant holds before the first iteration.
2. Maintenance: If the invariant holds before an iteration, it holds after.
3. Termination: The loop terminates and the invariant implies correctness.

Required Topics#

• Loop invariants
• Algorithm correctness proofs
• Binary search properties

Solution#

Solution coming soon.