Termination and correctness

When creating an algorithm, the following three criteria must be considered: termination, correctness and complexity.

The termination ensures that the algorithm ends after a certain number of elementary operations. The correctness ensures that the algorithm gives the expected result when it ends.

Example

A human being and a dog do not age the same way. To determine the human equivalent of the age of a dog less than 15kg, use the table below, where x is the actual age of the animal (in years), and y is the human equivalent in aging term.

complexity5

complexity6

Let’s check the termination. This is a conditioning suite with elementary calculations inside. Once all conditions are verified in order, the algorithm ends.

Let’s check the correctness. The algorithm does the operations described in the table.

Another example

In general, the termination is difficult to verify because we do not always know, a priori, the number of instructions. Correctness is complicated when one is in the presence of decision support or operational research. It is then necessary to use mathematical principles to prove that the algorithm is correct.

Take the example of the calculation of the gcd iterative.

complexity7

The algorithm ends if the stop condition of the loop is realized, ie if y is canceled. In the loop, y is replaced by a remainder modulo y. So at each passage, it decreases strictly while remaining positive or zero. As a result, it eventually reaches 0, so we leave the loop. The algorithm ends after a number of iterations.

Initially, x=a and y=b. In the loop, we replace (x,y) by (y,x mod y). We know that gcd(x,y)=gcd(y,x mod y). So at each iteration, gcd(x,y)=gcd(a,b). At the end of the loop, y=0, or gcd(x,0)=x. By induction we deduce that we return gcd(a,b). The algorithm calculates the desired gcd.

Tool for termination and correctness

A quantity which takes its values in a well-founded set and which decreases strictly with each passage in a loop is called convergent. A well-founded set is a totally ordered set in which there is no infinite sequence strictly decreasing. The existence of a convergent for a loop ensures that the algorithm eventually gets out. For example, in the case of Euclid’s algorithm, y is a convergent.

A loop invariant is a property that, if it is true when entering a loop, remains true after each pass in that loop. It is therefore true at the exit of this loop. The loop invariant is analogous to the recurrence principle. The highlighting of an adapted loop invariant makes it possible to prove the correctness of an algorithm. For example, gcd(a,b)=gcd(x,y) is a loop invariant.

We will take as an example a algorithm with a random variable to test the notions of termination and correction.

complexity8

In computer science, the random attributes a value in a range of value. The pseudo-random is either limited by the size of the container (int, double, etc.) or by the algorithm used (generation of a number modulo a very large number). In the algorithm, we assume that n and p are strictly positive integers. If they have an operation that makes it negative, then the value of 0 will be automatically assigned.

In the second part of the condition, x decreases while y has a random value (strictly bounded). x tends to the value 0. In the first part of the condition, y decreases to 0 from its random value. We conclude that the algorithm decreases y to 0, then decrements x before giving a new value to y. By recurrence we conclude that x tends to 0 after a random number of iterations, so that the second part will no longer be visited. And y also tends to 0, so we come out of the loop. So we have to prove that the algorithm ends. It is not useful to speak of correctness in this case since we did not have specifications to check.

It is noted that some algorithm has no proof of termination as the famous function of Syracuse.

 

Publicités