Invariant Based Programming

Invariant Based Programming

Discussion
 Ask a question about 'Invariant Based Programming' Start a new discussion about 'Invariant Based Programming' Answer questions from other users Full Discussion Forum

Encyclopedia
Invariant based programming is a programming methodology where specifications
Formal specification
In 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 invariants
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:...

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 correctness
Formal verification
In 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 semantics
Formal semantics of programming languages
In 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 loops
For loop
In 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 loops
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....

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. Dijkstra
Edsger Dijkstra
Edsger 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. Reynolds
John C. Reynolds
John 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 Back
Ralph-Johan Back
Ralph-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...

.