Invariant-based programming: Difference between revisions

Revision as of 18:19, 24 June 2007

Revision as of 18:41, 7 August 2007

Line 1:

{{Orphan|date=October 2006}} {{Uncategorized|date=June 2007}}

'''Invariant based programming''' 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 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 [[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 proofs is also possible.

Line 5:

The 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 in a number of different forms by M.H. van Emden, [[John C. Reynolds|J.C. Reynolds]] and [[Ralph-Johan Back|R-J Back]].

[[Category:Formal methods]]

[[Category:Programming paradigms]]