Informal example
The following Cmax()
returns the maximum value in its argument array a[]
, provided its length n
is at least 1.
Comments are provided at lines 3, 6, 9, 11, and 13. Each comment makes an assertion about the values of one or more variables at that stage of the function.
The highlighted assertions within the loop body, at the beginning and end of the loop (lines 6 and 11), are exactly the same. They thus describe an invariant property of the loop.
When line 13 is reached, this invariant still holds, and it is known that the loop condition i!=n
from line 5 has become false. Both properties together imply that m
equals the maximum value in a ...n-1/code>, that is, that the correct value is returned from line 14.
int max(int n, const int a[])
Following a defensive programming paradigm, the loop condition i!=n
in line 5 should better be modified to i, in order to avoid endless looping for illegitimate negative values of n
. While this change in code intuitively shouldn't make a difference, the reasoning leading to its correctness becomes somewhat more complicated, since then only i>=n
is known in line 13. In order to obtain that also i<=n
holds, that condition has to be included into the loop invariant. It is easy to see that i<=n
, too, is an invariant of the loop, since i in line 6 can be obtained from the (modified) loop condition in line 5, and hence i<=n
holds in line 11 after i
has been incremented in line 10. However, when loop invariants have to be manually provided for formal program verification, such intuitively too obvious properties like i<=n
are often overlooked.
Floyd–Hoare logic
In Floyd–Hoare logic
Hoare logic (also known as Floyd–Hoare logic or Hoare rules) 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 log ...
, the partial correctness
Partial may refer to:
Mathematics
* Partial derivative, derivative with respect to one of several variables of a function, with the other variables held constant
** ∂, a symbol that can denote a partial derivative, sometimes pronounced "partial ...
of a 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.
Overview
The '' ...
is governed by the following rule of inference:
:
This means:
* If some property is preserved by the code —more precisely, if holds after the execution of whenever both and held beforehand— ''(upper line)'' then
* and are guaranteed to be false and true, respectively, after the execution of the whole loop , provided was true before the loop ''(lower line)''.
In other words: The rule above is a deductive step that has as its premise the Hoare triple
Hoare logic (also known as Floyd–Hoare logic or Hoare rules) 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 log ...
. This triple is actually a relation
Relation or relations may refer to:
General uses
*International relations, the study of interconnection of politics, economics, and law on a global level
*Interpersonal relationship, association or acquaintance between two or more people
*Public ...
on machine states. It holds whenever starting from a state in which the boolean expression is true and successfully executing some code called , 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 will lead from a state in which is true to a state in which holds. The boolean formula in this rule is called a loop invariant.
With some variations in the notation used, and with the premise that the loop halts, this rule is also known as the Invariant Relation Theorem. As one 1970s textbook presents it in a way meant to be accessible to student programmers:
Let the notation P Q
mean that if P
is true before the sequence of statements seq
run, then Q
is true after it. Then the invariant relation theorem holds that
:P & c P
::implies
:P P & ¬c
Example
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 has to be guessed; it will turn out that is appropriate. 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 , 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 ( is less than or equal to 10, but it is not less than 10) is logically equivalent
Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from premises ...
to , which is what we wanted to show.
The property is another invariant of the example loop, and the trivial property is another one.
Applying the above inference rule to the former invariant yields .
Applying it to invariant yields , which is slightly more expressive.
Programming language support
Eiffel
The Eiffel
Eiffel may refer to:
Places
* Eiffel Peak, a summit in Alberta, Canada
* Champ de Mars – Tour Eiffel station, Paris, France; a transit station
Structures
* Eiffel Tower, in Paris, France, designed by Gustave Eiffel
* Eiffel Bridge, Ungheni, M ...
programming language provides native support for loop invariants. A loop invariant is expressed with the same syntax used for a class invariant
In computer programming, specifically object-oriented programming, a class invariant (or type invariant) is an invariant used for constraining objects of a class. Methods of the class should preserve the invariant. The class invariant constrain ...
. 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; this is checked at runtime.
from
x := 0
invariant
x <= 10
until
x > 10
loop
x := x + 1
end
Whiley
The Whiley Whiley is the surname of:
* Manning Whiley (1915–1975), British actor
* Richard Whiley (born 1935), English cricketer
* Jo Whiley (born 1965), English DJ
* Matthew Whiley (born 1980), English cricketer
* Jordanne Whiley (born 1992), British wheel ...
programming language also provides first-class support for loop invariants. Loop invariants are expressed using one or more where
clauses, as the following illustrates:
function max(int[] items) -> (int r)
// Requires at least one element to compute max
requires , items, > 0
// (1) Result is not smaller than any element
ensures all
// (2) Result matches at least one element
ensures some :
//
nat i = 1
int m = items //
while i < , items,
// (1) No item seen so far is larger than m
where all
// (2) One or more items seen so far matches m
where some :
if items > m:
m = items i = i + 1
//
return m
The max()
function determines the largest element in an integer array. For this to be defined, the array must contain at least one element. The postconditions In computer programming, a postcondition is a condition or predicate that must always be true just after the execution of some section of code or after an operation in a formal specification. Postconditions are sometimes tested using assertions wit ...
of max()
require that the returned value is: (1) not smaller than any element; and, (2) that it matches at least one element. The loop invariant is defined inductively through two where
clauses, each of which corresponds to a clause in the postcondition. The fundamental difference is that each clause of the loop invariant identifies the result as being correct up to the current element i
, whilst the postconditions identify the result as being correct for all elements.
Use of loop invariants
A loop invariant can serve one of the following purposes:
# purely documentary
# to be checked within in the code by an assertion call
# to be verified based on the Floyd-Hoare approach
For 1., a natural language comment (like // m equals the maximum value in a ...i-1/code> in the above example) is sufficient.
For 2., programming language support is required, such as the C library assert.h
assert.h is a header file in the standard library of the C programming language that defines the C preprocessor macro assert().International Standard for Programming Language C (C99), ISO/IEC 9899:1999, p. 169
In C++ it is also available thro ...
, or the above-shown invariant
clause in Eiffel. Often, run-time checking can be switched on (for debugging runs) and off (for production runs) by a compiler or a runtime option.
For 3., some tools exist to support mathematical proofs, usually based on the above-shown Floyd–Hoare rule, that a given loop code in fact satisfies a given (set of) loop invariant(s).
The technique of abstract interpretation
In computer science, abstract interpretation is a theory of sound approximation of the semantics of computer programs, based on monotonic functions over ordered sets, especially lattices. It can be viewed as a partial execution of a computer prog ...
can be used to detect loop invariant of given code automatically. However, this approach is limited to very simple invariants (such as 0<=i && i<=n && i%20
).
Distinction from loop-invariant code
Loop-invariant code consists of statements or expressions that can be moved outside a loop body without affecting the program semantics. Such transformations, called loop-invariant code motion
In computer programming, loop-invariant code consists of statements or expressions (in an imperative programming language) that can be moved outside the body of a loop without affecting the semantics of the program. Loop-invariant code motion (a ...
, are performed by some compilers to optimize programs.
A loop-invariant code example (in the C programming language
''The C Programming Language'' (sometimes termed ''K&R'', after its authors' initials) is a computer programming book written by Brian Kernighan and Dennis Ritchie, the latter of whom originally designed and implemented the language, as well as ...
) is
for (int i=0; i
where the calculations x = y+z
and x*x
can be moved before the loop, resulting in an equivalent, but faster, program:
x = y+z;
t1 = x*x;
for (int i=0; i
In contrast, e.g. the property 0<=i && i<=n
is a loop invariant for both the original and the optimized program, but is not part of the code, hence it doesn't make sense to speak of "moving it out of the loop".
Loop-invariant code may induce a corresponding loop-invariant property. For the above example, the easiest way to see it is to consider a program where the loop invariant code is computed both before and within the loop:
x1 = y+z;
t1 = x1*x1;
for (int i=0; i
A loop-invariant property of this code is (x1x2 && t1x2*x2) , , i0
, indicating that the values computed before the loop agree with those computed within (except before the first iteration).
See also
* Invariant (computer science)
In mathematics, an invariant is a property of a mathematical object (or a class of mathematical objects) which remains unchanged after operations or transformations of a certain type are applied to the objects. The particular class of objects ...
* Loop-invariant code motion
In computer programming, loop-invariant code consists of statements or expressions (in an imperative programming language) that can be moved outside the body of a loop without affecting the semantics of the program. Loop-invariant code motion (a ...
* Loop variant In computer science, a loop variant is a mathematical function defined on the state space of a computer program whose value is monotonically decreased with respect to a (strict) well-founded relation by the iteration of a while loop under some inva ...
* Weakest-preconditions of While loop
References
Further reading
* Thomas H. Cormen
Thomas H. Cormen is the co-author of ''Introduction to Algorithms'', along with Charles Leiserson, Ron Rivest, and Cliff Stein. In 2013, he published a new book titled '' Algorithms Unlocked''. He is a professor of computer science at Dartmout ...
, Charles E. Leiserson
Charles Eric Leiserson is a computer scientist, specializing in the theory of parallel computing and distributed computing, and particularly practical applications thereof. As part of this effort, he developed the Cilk multithreaded language. ...
, Ronald L. Rivest
Ronald Linn Rivest (; born May 6, 1947) is a cryptographer and an Institute Professor at MIT. He is a member of MIT's Department of Electrical Engineering and Computer Science (EECS) and a member of MIT's Computer Science and Artificial Inte ...
, and Clifford Stein
Clifford Seth Stein (born December 14, 1965), a computer scientist, is a professor of industrial engineering and operations research at Columbia University in New York, NY, where he also holds an appointment in the Department of Computer Scie ...
. ''Introduction to Algorithms
''Introduction to Algorithms'' is a book on computer programming by Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. The book has been widely used as the textbook for algorithms courses at many universities and is co ...
'', Second Edition. MIT Press and McGraw-Hill, 2001. . Pages 17–19, section 2.1: Insertion sort.
* David Gries
David Gries (born April 26, 1939 in Flushing, Queens, New York) is an American computer scientist at Cornell University, United States mainly known for his books ''The Science of Programming'' (1981) and ''A Logical Approach to Discrete Math'' ( ...
.
A note on a standard strategy for developing loop invariants and loops
" ''Science of Computer Programming'', vol 2, pp. 207–214. 1984.
* Michael D. Ernst, Jake Cockrell, William G. Griswold, David Notkin.
" ''International Conference on Software Engineering'', pp. 213–224. 1999.
* Robert Paige.
Programming with Invariants
" ''IEEE Software'', 3(1):56–69. January 1986.
* Yanhong A. Liu, Scott D. Stoller, and Tim Teitelbaum
(Ray) Tim Teitelbaum (born April 12, 1943, United States) is an American computer scientist known for his early work on Integrated development environment, integrated development environments (IDEs), Structure editing, syntax-directed editing, an ...
Strengthening Invariants for Efficient Computation
''Science of Computer Programming'', 41(2):139–172. October 2001.
* Michael Huth, Mark Ryan.
Logic in Computer Science
", Second Edition.
{{DEFAULTSORT:Loop Invariant
Formal methods
Control flow