I am currently being introduced to algorithms and I am trying to learn about showing the correctness. For training I chose the very basic linear-search algorithm and I would like to know if this is a correct proof. Thank you for your feedback!
function LinearSearch(Array A, int v): for j=1 in A.length: if A[j] == v: return A[j] endfor return NULL
Invariant: At the beginning of every iteration of the for-loop the subarray
[1,..., j-1] doesnt contain the searched element
j = 1 it's obvious that
v is not contained in the array before this iteration since
A doesn't exist.
Maintenance: For every new iteration it is certain that the subarray
A[1,..,j-1] doesn't contain
v and the invariant holds. If
v would have been part of the subarray the algorithm would have already terminated due to the if-clause.
v is not found earlier, the algorithm will terminiate by reaching
j > A.length = n and returning
NULL. In relation to the invariant this means that the subarray
[1,n] did not contain
v. Therefore the invariant is fulfilled and the algorithm terminates correctly.