Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > Semantics and Proof Rules of I...

Semantics and Proof Rules of Invariant Based Programs

Ralph-Johan Back, Viorel Preoteasa, Semantics and Proof Rules of Invariant Based Programs. TUCS Technical Reports 903, Turku Centre for Computer Science, 2008.

Abstract:

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.

Abstract The execution of an invariant diagram may start in any situation and will choose one of the enabled transitions in this situation, to continue to the next situation. In this way, the execution proceeds from situation to situation. Execution terminates when a situation is reached from which there are no enabled transitions. Because the execution could start and terminate in any situation, invariant-based programs can be thought of as multiple entry, multiple exit programs. The transitions may have statements with unbounded nondeterminism, because we allow specification statements in transitions. Invariant based programs are thus a considerable generalization of ordinary structured program statements, and defining their semantics and proof theory provides a challenge that usually does not arise for more traditional programming languages

Abstract We study in this paper the semantics and proof rules for invariant-based programs. The total correctness of an invariant diagram is established by proving that each transition preserves the invariants and decreases a global variant. The proof rules for invariant-based programs are shown to be correct and complete with respect to an operational semantics. The proof of correctness and completeness introduces the weakest precondition semantics for invariant diagrams, and uses a special construction, based on well-ordered sets, of the least fixpoint of a monotonic function on a complete lattice. The results presented in this paper have been mechanically verified in the PVS theorem prover.

Files:

Full publication in PDF-format

BibTeX entry:

@TECHREPORT{tBaPr08a,
  title = {Semantics and Proof Rules of Invariant Based Programs},
  author = {Back, Ralph-Johan and Preoteasa, Viorel},
  number = {903},
  series = {TUCS Technical Reports},
  publisher = {Turku Centre for Computer Science},
  year = {2008},
  keywords = {Invariant based programming. Semantics. Hoare proof rules. Completeness},
  ISBN = {978-952-12-2111-8},
}

Belongs to TUCS Research Unit(s): Software Construction Laboratorium

Edit publication