Is this loop invariant correct?
<p><strong>The pseudocode for linear search loop:</strong></p>

<pre><code>for j = 1 to A.length 
   if(A[j] = v) 
      return j;
return NIL
</code></pre>

<p><strong>Loop invariant I've written:</strong></p>

<p>At the start of each iteration of the for loop, <em>j</em> is the next index after where <em>A[j-1]</em> doesn't equal <em>v</em>. </p>

<p><strong>Initialization:</strong></p>

<p>When <em>j</em> equals <em>1</em> and before checking whether it is lesser than <em>A.length</em>, the previous index is <em>0</em>. Then <em>A[0]</em> doesn't equal to <em>v</em>, because in this context <em>A[0]</em> doesn't even exist. </p>

<p><strong>Maintenance:</strong> </p>

<p>If <em>A[j]</em> equals <em>v</em> then loop terminates. Which means we don't have next iteration. But if it doesn't equal to <em>v</em> then next iteration of the loop executes while preserving the loop invariant. </p>

<p><strong>Termination:</strong></p>

<p>The conditions causing the for loop to terminate are that <em>j</em> is bigger than <em>A.length</em> or <em>v</em> equals <em>A[j]</em>. Because each loop iteration increases <em>j</em> by <em>1</em>, we have checked every elements of <em>A</em> against <em>v</em> until <em>j</em> is bigger than <em>A.length</em>. Hence the algorithm is correct. If <em>v</em> equals <em>A[j]</em> then it means the we have found the element we've been searching. Thus the algorithm is correct. </p>

<p>Are these correct? </p>