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. 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 proved 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 complex 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 a 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 of time. Let the algorithm consists 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 then postcondition must 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 a real-life problem often involves a loop. The correctness of such algorithm is proved through 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, invariant gives us a useful property that helps us to prove the correctness of the algorithm.
Correctness does not involve analysis of the algorithm
Prove the correctness of Insertion sort
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]. Remaining A[j…n] cards are unsorted.
Let us try to prove the correctness of INSERTION_SORT using three-loop invariant properties.
The loop invariant holds before initialization. For j = 2, subarray A[1…j – 1] contains only one element, i.e. A. This is a trivial case of sorting. It proves that the loop invariant is true before the first iteration.
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 to 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 hold in attendance too.
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