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. In: William Chu, W. Eric Wong, Mathew J. Palakal, Chih-Cheng Hung, Jan Cederquist (Eds.), SAC '11 Proceedings of the 2011 ACM Symposium on Applied Computing, 1658–1665, ACM New York, NY, USA, 2011.

http://dx.doi.org/10.1145/1982185.1982532

Abstract:

Invariant based programming is an approach where we start to con-
struct a program by first identifying the basic situations (pre- and
postconditions as well as invariants) that could arise during the ex-
ecution 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 con-
structing the program. The program structure in invariant based
programs is determined by the information content of the situa-
tions, 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.

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 dia-
grams, 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:

@INPROCEEDINGS{inpBaPr11a,
  title = {Semantics and Proof Rules of Invariant Based Programs},
  booktitle = {SAC '11 Proceedings of the 2011 ACM Symposium on Applied Computing},
  author = {Back, Ralph-Johan and Preoteasa, Viorel},
  editor = {Chu, William and Wong, W. Eric and Palakal, Mathew J. and Hung, Chih-Cheng and Cederquist, Jan},
  publisher = {ACM New York, NY, USA},
  pages = {1658–1665},
  year = {2011},
}

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

Publication Forum rating of this publication: level 1

Edit publication