Is this a good proof of correctness?

Question

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[0] 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.

Answer 1

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.