Answer:
1 for i = 1 to A.length
2 if A[i] = nu
3 return i
4 return NIL
Explanation:
Loop invariant:
At the start of each iteration of the for loop of lines 1-3, there is no j<i such that A[j]=ν.
Initialization:
At the beginning of the first iteration, we have i=1, so there is no j<i such that A[j]=ν.
Maintenance:
We fix i and assume there is no j<i such that A[j]=ν.
If A[i]=ν, then we return a value, so then there are no more iterations, so the property is preserved.
If A[i]≠ν, then there is no j<i+1 such that A[j]=ν, which is the desired property for the next step.
Termination:
The loop terminates either for i=A.length+1, or if ever we encounter A[i]=ν.
In the first case, then there is no 1≤j≤A.length such that A[j]=ν, and we are correctly returning NIL
In the second case, if we encounter some i such that A[i]=ν, we are correctly returning i.
