Loop invariant
In computer science , a loop invariant is a special form of the invariant that is valid at the beginning and end of each loop pass and before and after the execution of the loop in an algorithm . It is therefore independent of the number of its current runs. A loop invariant is required for the formal verification of algorithms and also helps to better capture the processes within a loop. Typically, loop invariants describe value ranges of variables and relationships between the variables. Since the loop invariant is a logical expression, it can be either true or false.
For each loop an invariant can be found that applies before the loop and after each test of the loop condition, e.g. B. a tautology like "true = true". An invariant can always be determined, but this is not always suitable for carrying out a formal proof of correctness.
Proof of correctness
According to the Hoare calculus , a loop invariant must be used to prove the correctness of a loop that the loop invariant is valid immediately before the loop is executed and after each test of the loop condition. After checking the loop condition, the loop can either be entered (loop condition fulfilled) or exited (loop condition not fulfilled). Therefore, the invariant must apply both at the beginning of each loop pass and directly after the loop (see example).
Partial correctness
For the partial correctness check, you first check whether the invariant applies at the first critical point in time, i.e. directly before the loop. It is then checked whether it is retained when moving from one round to the next. This procedure corresponds to the complete induction of mathematics. In addition, the invariant must also apply directly after the loop. The loop invariant must be correct at all three times, i.e. H. Variables must e.g. B. lie within defined areas or have certain relationships with each other.
After leaving a loop in which the invariant is not violated, the rejecting loop condition apply (otherwise the loop would not have been exited) and the loop invariant. If these two logical expressions give the desired result of the loop using and-operation, then the partial correctness of the loop has been proven. Partial correctness means that whenever the loop is terminated (exited), the correct result is available. However, this does not prove that the loop always terminates (total correctness).
Total correctness
In order to prove the total correctness of a loop, the partial correctness must first be proven. It is then checked whether the loop always terminates. To do this, it must first be determined when the loop can be left. If it can be exited, it must be demonstrated that it does so in any case, e.g. B. the counter variable of a for loop increases with each pass up to an upper limit and is not changed within the loop.
If it is proven in this way that the loop always terminates and that the desired result is always available afterwards, the total correctness of the loop is proven.
It has been proven that there is no algorithm that automatically finds a loop invariant for all loops that can be used for a proof of correctness.
example
The following algorithm multiplies the two variables a and b together:
1 multiply(a, b) {
2 x := a;
3 y := b;
4 p := 0;
5 // die Invariante muss vor der Schleife gelten
6 while x > 0 do {
7 // die Invariante muss am Anfang jedes Durchlaufs gelten
8 p := p + y;
9 // innerhalb der Schleife muss die Invariante nicht gelten;
10 // (x * y) + p = a * b ist an dieser Stelle nicht erfüllt
11 x := x - 1;
12 // die Invariante muss auch am Ende jedes Durchlaufs gelten
13 }
14 // die Invariante muss auch direkt nach der Schleife gelten
15 return p
16 }
A loop invariant for this algorithm is:
Native support from programming languages
Eiffel
The Eiffel programming language natively offers loop invariants. The invariants are monitored by the programming language at runtime.
The following example x <= 10defines the invariant for the loop. The loop runs until it reaches xthe value 10. Then the loop is exited. In the example, the invariant is fulfilled both before the execution of the loop and after each execution of the loop.
from
x := 0
invariant
x <= 10
until
x >= 10
loop
x := x + 1
end
See also
Individual evidence
- ↑ Martin Glinz, Harald Gall: Systematic programming: Writing readable and changeable programs . In: Software Engineering . 2005, p. 39–40 ( ifi.uzh.ch [PDF; accessed April 11, 2014]).
- ^ Edsger Wybe Dijkstra : Some beautiful arguments using mathematical induction . In: Acta Informatica . No. 13 , 1980, pp. 1-8 .
- ^ Bertrand Meyer : Eiffel: The Language . Prentice Hall, 1991, pp. 129-131.