How would I Prove the algorithm correct using the initialization-maintenance-termination technique?

Question

And what would be the conditions that must be met during execution of the function? (Assertion)

I want to make sure that my assertion would describe what I know is true after running the ith loop.

int linearsearch(int arr[], int n, int target) {
    for (int i = 0; i < n; i++) {
        if (arr[i] == target) return i;
    }
    return -1;
}

This is just an iterative linear search function that returns the index of the target if the target is found and -1 otherwise.

Answer 1

Loop invariant for the problem of linear search must make a statement about all array elements that were previously searched, namely, that none of them is equal to target:

∀ j < i : arr_j ≠ target

You need to prove several points about it:

• Show that the invariant holds before entering the loop
• Show that if the invariant holds before an iteration, it also holds upon completion of the iteration
• Show that if the loop ends through return in the middle, the algorithm produces the correct result
• Show that if the loop ends normally, the algorithm also produces the correct result