Is this loop invariant and its informal proof correct? (CLRS 3rd ed. exercise 2-1-3)

Question

Given the following algorithm for linear-search (referring to index 1 as the index of the first element in an array of elements):

found_idx = nil
for i = 1 to A.length
  if A[i] == value
    found_idx = i
    return found_idx
  end-if
end-for
found_idx

I was wondering if this loop-invariant is correct: " At the start of each iteration of the for-loop, found_idx is the index in the array ending at i-1 at which value exists if that value exists"

Here is my proposed informal explanation of this loop-invariant according to the format in CLRS:

1. Initialization: This is true before the first iteration because i = 1 and the array ending at i-1 is empty, and found_idx is therefore nil.
2. Maintenance: This is true after each iteration because at each value of i, A[i] is checked and then i is incremented, meaning that all elements up to i-1 have been checked prior to each new iteration.
3. Termination: This terminates when i > A.length, meaning that all elements up to and including A.length have been checked.

My main point of concern is that it feels incorrect to refer to the index ending at i-1 because the loop starts with i at 1, which is the first element of the array. In other words, it feels fallacious to refer to a subarray of an array, wherein the subarray ends at an index less than the starting index of the array for which the subarray is supposed to be a subarray in the first place. This seems to imply that the loop invariant given above is actually false before the very first iteration of the loop.

Thoughts?

Answer 1

Since the loop terminates early, its invariant is as follows:

found_idx = nil && ∀k<i : A[k] ≠ value

The part after && means "All of A's elements at indexes below i are not equal to value".

• This is trivially true before entering the loop
• Conditional either keeps found_idx at nil, or terminates the loop early
• Loop terminates when i reaches A.length

Loop's post-condition is found_idx = nil && ∀k<A.length : A[k] ≠ value, which simply means that value is not among A's elements. It also means that you can eliminate found_idx by rewriting your loop as follows:

for i = 1 to A.length
    if A[i] == value
        return i
    end-if
end-for
return nil