Correctness of Algorithm – Concept and Proof

Why correctness of Algorithm is essential?

Proving correctness of algorithm is crucial. For many problems, algorithms are very complex. The reliability of an algorithm cannot be claimed unless and until it gives the correct output for each of the valid inputs.

Tracing the output of each possible input is impossible. The correctness of an algorithm can be quickly proven by checking certain conditions.

Programming languages are an effective means of implementing complicated packages and applications. Complex systems, such as banking and e-commerce, are difficult to design and evaluate and are frequently incorrect. Much has been said regarding the creation of an effective tool for developing dependable software.

We consider software to be “right” if it performs precisely what the programmer and user want it to do. Millions of lines of code are used in modern software, which includes thousands of states and state transitions. Claiming the dependability of such software is not a simple process; it must go through all possible input scenarios to determine whether or not it is giving the proper output.

Rather than checking all instances of input, correctness can be proved easily by mathematical models.

Confirming Correctness of Algorithm

The well-defined computational problem is a triplet of
P (I, O, R) such that I is the valid input set, O is the accepted output set, and R defines the relationship between I and O. R can be considered as a mapping function, which translates I to R. Let i ∈ I is a problem instance.

The algorithm to solve problem P is correct if and only if for all the problem instance i ∈ I, it terminates and produces correct output o ∈ O, i.e. (i, o) ∈ R.

It is necessary to prove the correctness of the algorithm. The simplest way of doing so is to test the algorithm for different input combinations and compare the results with manually computed or already available ground truth values

However, a testing algorithm for all inputs is not possible, or it may take too much time. Let the algorithm consist of a series of n steps.

One way to prove the correctness of the algorithm is to check the condition before (precondition) and after (postcondition) the execution of each step.

The algorithm is correct only if the precondition is true, and then the postcondition must also be true.

Consider the problem of finding the factorial of a number n.  The algorithm halts after doing (n – 1) multiplications. Proving the correctness of this problem informally is very simple. But for large inputs, it becomes tedious to store a huge output.

Algorithms for real-life problems often involve a loop. The correctness of such an algorithm is proved through the loop invariant property. It involves three steps:

Initialization: Conditions true before the first iteration of the loop

Maintenance: If the condition is true before the loop, it must be true before the next iteration.

Termination: On termination of the loop, the invariant gives us a useful property that helps us prove the correctness of the algorithm.

Correctness does not involve analysis of the algorithm

Prove the correctness of Insertion sort

The algorithm for insertion sort is given below.

Algorithm INSERTION_SORT(A, n)

for j ← 2 to n do
  Key ← A[j]
  i ← j – 1 
  while i > 0 && key < A[i] do
    A[i + 1] ← A[i]
    i ← i – 1
  end
  A[i + 1] ← key
end

First, j cards are always sorted in array A[1…j – 1]. The remaining A[j…n] cards are unsorted.

Let us try to prove the correctness of INSERTION_SORT using three-loop invariant properties.

Initialization:

The loop invariant holds before initialization. For j = 2, subarray A[1…j – 1] contains only one element, i.e. A[1]. This is a trivial case of sorting. It proves that the loop invariant is true before the first iteration.

Maintenance:

In each iteration, the algorithm finds the correct position of the key to insert the element A[j] by moving A[j – 1], A[j – 2],.. elements. After the loop, A[j] element will be inserted into the correct position. After the loop, A[1…j] contains elements the same as in A[1…j] before the loop, but now they will be in sorted order. Thus the invariant is held in attendance too.

Termination:

The loop terminates when j = n. Each iteration inserts A[j] on the correct location, so after n iteration, all elements will be in their right position. After the loop, A[1…n] contains elements the same as in A[1…n] before the loop, but now they will be in sorted order.

---

Additional Reading: Click to read few more examples

Short Questions:

Q: Why proving correctness is important?

Tracing the output of each possible input is impossible. The correctness of an algorithm can be quickly proved by checking certain conditions.

Q: Which are the steps for loop invariant?

Loop invariant involves:

• Initialization: Conditions true before the first iteration of the loop
• Maintenance: If the condition is true before the loop, it must be true before the next iteration.
• Termination: On termination of the loop, the invariant gives us a useful property that helps us to prove the correctness of the algorithm.