Invariant-based programming
Invariant based programming is a programming methodology where specifications and 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 correctness of the program based on the formal semantics of program statements. A high degree of automation of such proofs is also possible.
Writing invariants before program statements has been considered before in a number of different forms by, e.g, M.H. van Emden, E.W. Dijkstra, J.C. Reynolds and 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 loops, while loops and if 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.