Loop Invariant
A loop invariant is a condition or property that is true at the beginning and end of every iteration of a loop. Loop invariants are key to proving correctness of iterative algorithms.
For example, in a linear search:
Java:
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
| int search(int[] arr, int x) {
int i = 0;
// Loop invariant:
// If x is in arr, then x is in arr[0..i]
while (i < arr.length) {
if (arr[i] == x) {
return i;
}
i++;
}
return -1;
}
|
C++:
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
| int search(vector<int>& arr, int x) {
int i = 0;
// Loop invariant:
// If x is in arr, then x is in arr[0..i]
while (i < arr.size()) {
if (arr[i] == x) {
return i;
}
i++;
}
return -1;
}
|
Python:
1
2
3
4
5
6
7
8
9
10
11
12
| def search(arr, x):
i = 0
# Loop invariant:
# If x in arr, x is in arr[0..i]
while i < len(arr):
if arr[i] == x:
return i
i += 1
return -1
|
Loop invariants describe what must remain true before and after each loop iteration for algorithm correctness.