# Is this a good proof of correctness?

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!

Algorithm-Pseudocode:

function LinearSearch(Array A, int v):
for j=1 in A.length:
if A[j] == v:
return A[j]
endfor
return NULL


My proof:

Invariant: At the beginning of every iteration of the for-loop the subarray [1,..., j-1] doesnt contain the searched element v.

Initialization: For 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.

Termination: If 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.

• We discourage "please check whether my answer is correct" questions, as only "yes/no" answers are possible, which won't help you or future visitors. See here and here. Can you edit your post to ask about a specific conceptual issue you're uncertain about? As a rule of thumb, a good conceptual question should be useful even to someone who isn't looking at the problem you happen to be working on. If you just need someone to check your work, you might seek out a friend, classmate, or teacher.
– D.W.
Jul 18, 2022 at 9:13

LinearSearch( Array A, int v):

{ forall i<1: A[i] != v } (vacuously true)
for j= 1 in A.length:
{ forall i<j: A[i] != v } (invariant)
if A[j] == v:
return A[j] {A[j] == v} (this postcondition is sufficient)
{ forall i<j+1: A[i] != v } (by conjunction of the invariant and "else" condition)
endfor

{ forall i<A.length+1: A[i] != v } (invariant and exit condition of the loop)
return NULL


If you wand to be picky, you can prove that the algorithm returns the first occurrence of v in the array. In this case, the postcondition is a little stronger.

Note that the algorithm is so simple that it can be proven in a straightforward way.

1. if the algorithm returns a non NULL, the condition A[j] == v holds for some j, proving that v was found;

2. if the algorithm returns NULL, every A[j] has been tested (the loop is a pure for) and found different from v.