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.

You need to assume that `arr` points to at least `n` ints (contained in the same object I suppose). Then you naturally get that `arr!=NULL` and `n<=SIZE_MAX`. If you don't make this assumption, `arr[i]` may cause undefined behavior, invalidating your proof. — Paul Hankin, Jun 15 '17 at 07:48

score 2 · Answer 1 · edited Jun 20 '20 at 09:12

2

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

edited Jun 20 '20 at 09:12

Community

1
1

answered Jun 15 '17 at 00:49

Sergey Kalinichenko

714,442
84
1,110
1,523

I think you must also assume that `arr` points to at least `n` ints. – Paul Hankin Jun 15 '17 at 07:46

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

1 Answers1

∀ j < i : arrj ≠ target

∀ j < i : arr_j ≠ target