Invariant based programming is a programming methodology where
specificationsIn computer science, a formal specification is a mathematical description of software or hardware that may be used to develop an implementation. It describes what the system should do, not how the system should do it...
and
invariantsIn 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:...
are written before the actual program statements. Writing down the invariants during the programming process has a number of advantages: it requires the programmer to make his intentions about the program behavior explicit before actually implementing it, and invariants can be evaluated dynamically during execution to catch common programming errors. Furthermore, if strong enough, invariants can be used to prove the
correctnessIn the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics .- Usage :Formal verification can be...
of the program based on the
formal semanticsIn programming language theory, semantics is the field concerned with the rigorous mathematical study of the meaning of programming languages and models of computation...
of program statements. A combined programming and specification language, connected to a powerful formal proof system, will generally be required for full verification of non-trivial programs. In this case a high degree of automation of proofs is also possible.
In most existing programming languages the main organizing structures are control flow blocks such as
for loopsIn computer science a for loop is a programming language statement which allows code to be repeatedly executed. A for loop is classified as an iteration statement....
,
while loopsIn 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....
and
if statements. Such languages may not be ideal for invariants-first programming, since they force the programmer to make decisions about control flow before writing the invariants. Furthermore, most programming languages do not have good support for writing specifications and invariants, since they lack quantifier operators and one can typically not express higher order properties.
The idea of developing the program together with its proof originated from
E.W. DijkstraEdsger Wybe Dijkstra ; ) was a Dutch computer scientist. He received the 1972 Turing Award for fundamental contributions to developing programming languages, and was the Schlumberger Centennial Chair of Computer Sciences at The University of Texas at Austin from 1984 until 2000.Shortly before his...
. Actually writing invariants before program statements has been considered in a number of different forms by M.H. van Emden,
J.C. ReynoldsJohn C. Reynolds is an American computer scientist.John Reynolds studied at Purdue University and then earned a PhD in theoretical physics from Harvard University in 1961. He was Professor of Information science at Syracuse University from 1970 to 1986. Since then he has been Professor of Computer...
and
R-J BackRalph-Johan Back is a Finnish computer scientist.Back originated the refinement calculus, an important approach to the formal development of programs using stepwise refinement, in his 1978 PhD thesis at the University of Helsinki, On the Correctness of Refinement Steps in Program Development. He...
.