Invariant-based programming: Difference between revisions

Revision as of 16:48, 8 March 2006

Latest revision as of 02:36, 15 January 2025

(24 intermediate revisions by 20 users not shown)

Line 1:

{{Short description|Methodology of programming}}

'''Invariant -based programming'''<ref>Back, Ralph-Johan: [https://hal.archives-ouvertes.fr/hal-00477903/document Invariant Based Programming: Basic approach and Teaching Experience], Formal Aspects of Computing, 14 February 2008, ISSN 0934-5043 (Print) 1433-299X (Online)</ref> is a programming methodology where [[Formal specification|specifications]] and [[Invariant (computer science)|invariants]] 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 histheir 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 [[Formal verification|correctness]] of the program based on the [[Formal semantics of programming languages|formal semantics]] 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 such proofs is also possible.

MostIn most existing programming languages are not ideal for invariants-first programming, since the main organizing structures in algorithmic code are control flow blocks such as [[For loop|<ttcode>for</ttcode> loops]], [[While loop|<ttcode>while</ttcode> loops]] and [[If statement|<ttcode>if</ttcode> statements]]. ThisSuch forceslanguages may not be ideal for invariants-first programming, since they force the programmer to make decisions about control flow before writing the invariants, which should be avoided. 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 such as permutation of arrays well.

Writing invariants before program statements has been considered before in a number of different forms by, e.g, M.H. van Emden, [[Edsger Dijkstra|E.W. Dijkstra]], [[John_C._Reynolds|J.C. Reynolds]] and [[Ralph-Johan Back|R-J Back]].

WritingThe idea of developing the program together with its proof originated from [[Edsger Dijkstra|E.W. Dijkstra]]. Actually writing invariants before program statements has been considered before in a number of different forms by, e.g, M.H. van Emden, [[EdsgerJohn Dijkstra|E.WC. Dijkstra]], [[John_C._ReynoldsReynolds|J.C. Reynolds]] and [[Ralph-Johan Back|R-J Back]].

Most existing programming languages are not ideal for invariants-first programming, since the main organizing structures in algorithmic code are control flow blocks such as [[For loop|<tt>for</tt> loops]], [[While loop|<tt>while</tt> loops]] and [[If statement|<tt>if</tt> statements]]. This forces the programmer to make decisions about control flow before writing the invariants, which should be avoided. 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 such as permutation of arrays well.

== LinksSee also ==

* [[Eiffel (programming language)]]

== References ==

[http://www.abo.fi/~backrj/index.php?page=Invariant%20based%20programming.html Invariant based programming research by R-J Back]

<references/>

[[Category:ComputerFormal sciencemethods]]

[[Category:Programming paradigms]]