Scribd
Upload
6 views2 pages

Binary Search Algorithm Explained

The document describes the Binary Search algorithm, which efficiently finds a target value in a sorted array by repeatedly dividing the search interval in half. It includes a loop invariant that ensures the target is within the bounds defined by `low` and `high`, and provides a proof of correctness through initialization, maintenance, and termination. If the target is found, the algorithm returns its index; otherwise, it returns -1.

Uploaded by

Kira
Copyright
© All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd
6 views2 pages

Binary Search Algorithm Explained

The document describes the Binary Search algorithm, which efficiently finds a target value in a sorted array by repeatedly dividing the search interval in half. It includes a loop invariant that ensures the target is within the bounds defined by `low` and `high`, and provides a proof of correctness through initialization, maintenance, and termination. If the target is found, the algorithm returns its index; otherwise, it returns -1.

Uploaded by

Kira
Copyright
© All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd

Binary Search Algorithm

Algorithm:

BinarySearch(array, target):

low <- 0

high <- length(array) - 1

while low <= high do:

mid <- (low + high) // 2

if array[mid] == target then:

return mid // Target found at index mid

else if array[mid] < target then:

low <- mid + 1 // Search in the right half

else:

high <- mid - 1 // Search in the left half

return -1 // Target not found

Loop Invariant:

At the start of each iteration of the while loop, the target value (if it exists) is within the bounds

defined by `low` and `high`. More formally:

- If `target` exists in `array`, then `target` is in the subarray `array[low...high]`.

Proof of Correctness:

1. Initialization: Before the first iteration of the loop, `low` is initialized to `0` and `high` to

`length(array) - 1`. If the target is in the array, it is indeed within the bounds of `0` and `length(array)

- 1`, thus the invariant holds true.


2. Maintenance: Assume the loop invariant holds at the beginning of an iteration. During each

iteration, we compute `mid` as `(low + high) // 2`. Depending on the comparison of `array[mid]` with

`target`, we adjust either `low` or `high`:

- If `array[mid] < target`, we update `low` to `mid + 1`.

- If `array[mid] > target`, we update `high` to `mid - 1`.

- If `array[mid] == target`, we return `mid`, confirming that the target is found.

In each case, the invariant continues to hold, as we are narrowing the search space.

3. Termination: The loop terminates when `low` exceeds `high`. If the target has not been found, it

implies that the target does not exist in the array. The algorithm correctly returns `-1`.

You might also like