Semantics and proof rules of invariant based programs

Abstract

Invariant based programming is an approach where we start to construct a program by first identifying the basic situations (pre- and postconditions as well as invariants) that could arise during the execution of the algorithm. These situations are identified before any code is written. After that, we identify the transitions between the situations, which will give us the flow of control in the program. The transitions are verified at the time when they are constructed. The correctness of the program is thus established as part of constructing the program. The program structure in invariant based programs is determined by the information content of the situations, using nested invariant diagrams. The control structure is secondary to the situation structure, and will usually not be well-structured in the classical sense, i.e., it is not necessarily built out of single-entry single-exit program constructs.