Termination and Correction

Termination and correction

When creating a algorithm, the following three criteria must be taken into account: termination, correction and complexity.

Termination guarantees that the algorithm terminates after a certain number of elementary operations. The correction ensures that the algorithm gives the expected result when it terminates.

Example

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

termination and correction algorithm

Consider the following algorithm:

termination and correction algorithm

Let's check the termination. It is a conditioning suite with elementary calculations inside. Once all the conditions have been verified in order, the algorithm ends.

As regards the correction, the algorithm performs the operations described in the table.

Difficult example

In general, the termination is difficult to verify because we do not always know, a priori, the number of instructions carried out. The correction is complicated when one is in the presence ofhelp with the decision or operations research. It is then necessary to use principles math to prove that the algorithm is correct.

Let us take the example of calculating the gcd in iterative mode.

termination and correction algorithm

The algorithm ends if the stop condition of the loop is fulfilled, ie if y is canceled. In the loop, y is replaced by a modulo y remainder. So with each passage, strictly decreases while remaining positive or zero. Therefore, y ends up reaching 0, then we exit the loop. The algorithm ends well after a certain number of iterations.

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

Tool for termination and correction

We call convergent a quantity which takes its values in a well-founded set and which strictly decreases with each passage in a loop. A well-founded set is a totally ordered set in which there is no strictly decreasing infinite sequence. The existence of a convergent for a loop guarantees that the algorithm ends up exiting it. For example, in the case of Euclid's algorithm, y is a convergent.

We call a loop invariant a property which, if it is true when entering a loop, remains true after each passage through that loop. It is therefore true at the exit of this loop. The loop invariant is analogous to the principle of induction. The demonstration of an adapted loop invariant makes it possible to prove the correctness of an algorithm. For example, pgcd (a, b) = pgcd (x, y) is a loop invariant.

We will take as an example an algorithm with randomness in order to test the notions of termination and correction.

termination and correction algorithm

In computer science, randomness attributes a value in a range of values. 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 these have an operation making 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 therefore tends towards the value 0. In the first part of the condition, y decreases towards 0 from its random value. We therefore conclude that the algorithm decreases y to 0, then decrements x before giving a value to y again.

By induction we conclude that x will tend to 0 after a certain number of iterations, so that the second part will no longer be visited. And y also tends to 0, so we exit the loop. We have therefore proved that the algorithm terminates. It is not useful to talk about correction in this case since we had no specifications to check.

It is noted that some algorithm does not have proof of termination than the famous Syracuse function.

To share
en_GBEN
%d bloggers like this: