Loop invariant - AbsoluteAstronomy.com

Computer science

Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...

, a loop invariant is an invariant

Invariant (computer science)

In computer science, a predicate is called an invariant to a sequence of operations provided that: if the predicate is true before starting the sequence, then it is true at the end of the sequence.-Use:...

used to prove properties of loops. Informally, a loop invariant is a statement of the conditions that should be true on entry into a loop and that are guaranteed to remain true on every iteration of the loop. This means that on exit from the loop both the loop invariant and the loop termination condition can be guaranteed.

Specifically in Floyd-Hoare logic

Hoare logic

Hoare logic is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and logician C. A. R. Hoare, and subsequently refined by Hoare and other researchers...

, the partial correctness of a while loop

While loop

In most computer programming languages, a while loop is a control flow statement that allows code to be executed repeatedly based on a given boolean condition. The while loop can be thought of as a repeating if statement....

is governed by the following rule of inference:

This means:

A while loop does not have the side effect of falsifying —if the loop's body does not change an invariant from true to false given the condition , then will still be true after the loop has run as long as it was true before.
runs as long as the condition is true—after the loop has run, if it terminates, is false.

The rule above is a deductive step that has as its premise the Hoare triple

. This triple is actually a relation

Relation (mathematics)

In set theory and logic, a relation is a property that assigns truth values to k-tuples of individuals. Typically, the property describes a possible connection between the components of a k-tuple...

on machine states. It holds whenever starting from a state in which the boolean expression

is true and successfully executing some program called body, the machine ends up in a state in which

is true. If this relation can be proven, the rule then allows us to conclude that successful execution of the program while (C) body will lead from a state in which

is true to a state in which

holds. The boolean formula I in this rule is known as the loop invariant.

The following example illustrates how this rule works. Consider the program

while (x<10) x:=x+1;

One can then prove the following Hoare triple:

The condition C of the while loop is

. A useful loop invariant I is

. Under these assumptions it is possible to prove the following Hoare triple:

While this triple can be derived formally from the rules of Floyd-Hoare logic governing assignment, it is also intuitively justified: Computation starts in a state where

is true, which means simply that

is true. The computation adds 1 to x, which means that

is still true (for integer x).

Under this premise, the rule for while loops permits the following conclusion:

However, the post-condition

(x is less than or equal to 10, but it is not less than 10) is logically equivalent

Logical equivalence

In logic, statements p and q are logically equivalent if they have the same logical content.Syntactically, p and q are equivalent if each can be proved from the other...

, which is what we wanted to show.

The loop invariant plays an important role in the intuitive argument for soundness of the Floyd-Hoare rule for while loops. The loop invariant has to be true before each iteration of the loop body, and also after each iteration of the loop body. Since a while loop is precisely the repeated iteration of the loop body, it follows that if the invariant is true before entering the loop, it must also be true after exiting the loop.

Because of the fundamental similarity of loops and recursive

Recursion

Recursion is the process of repeating items in a self-similar way. For instance, when the surfaces of two mirrors are exactly parallel with each other the nested images that occur are a form of infinite recursion. The term has a variety of meanings specific to a variety of disciplines ranging from...

programs, proving partial correctness of loops with invariants is very similar to proving correctness of recursive programs via induction

Mathematical induction

Mathematical induction is a method of mathematical proof typically used to establish that a given statement is true of all natural numbers...

. In fact, the loop invariant is often the inductive property one has to prove of a recursive program that is equivalent to a given loop.

Eiffel

The Eiffel

Eiffel (programming language)

Eiffel is an ISO-standardized, object-oriented programming language designed by Bertrand Meyer and Eiffel Software. The design of the language is closely connected with the Eiffel programming method...

programming language provides native support for loop invariants. A loop invariant is expressed with the same syntax used for a class invariant

Class invariant

In computer programming, specifically object-oriented programming, a class invariant is an invariant used to constrain objects of a class. Methods of the class should preserve the invariant. The class invariant constrains the state stored in the object....

. In the sample below, the loop invariant expression x <= 10 must be true following the loop initialization, and after each execution of the loop body.

from
x := 0
invariant
x <= 10
until
x = 10
loop
x := x + 1
end

Eiffel

See also

Further reading