• TUCS Publication Series
• How to Publish in TUCS Series
• Publication Search
• Publication Graph
• Publication Input
• Publication Input Guide
• JuFo Browser

Invariant Based Programming: Basic approach and Teaching Experience

Ralph - Johan R Back, Invariant Based Programming: Basic approach and Teaching Experience. Formal Aspects of Computing , 2008.

Abstract:

Program verification is usually done by adding specifications and invariants to the program and
then proving that the verification conditions are all true. This makes program verification an
alternative to or a complement to testing. We describe here another approach to program
construction, which we refer to as invariant based programming, where we start by formulating
the specifications and the internal loop invariants for the program, before we write the program
code itself. The correctness of the code is then easy to check at the same
time as one is constructing it. In this approach, program verification becomes a complement to
coding rather than to testing. The purpose is to produce programs and software that are correct
by construction. We present a new kind of diagrams, nested invariant diagrams, where program
specifications and invariants (rather than the control) provide the main organizing structure.
Nesting of invariants provide an extension hierarchy that allows us to express the invariants in a
very compact manner. We have studied the feasibility of formulating specifications and loop
invariants before the code itself has been written in a number of case studies. Our experience is
that a systematic use of figures, in combination with a rough idea of the intended behavior of
the algorithm, makes it rather straightforward to formulate the invariants needed for the
program, to construct the code around these invariants and to check that the resulting program
is indeed correct. We describe our experiences from using invariant based programming in
practice, both from teaching programmers how to construct programs that they prove correct
themselves, and from teaching invariant based programming for CS students in class.

Files:

Full publication in PDF-format

BibTeX entry:

@ARTICLE{jBack08b,
  title = {Invariant Based Programming: Basic approach and Teaching Experience},
  author = {Back, Ralph - Johan R},
  journal = {Formal Aspects of Computing},
  year = {2008},
}

Belongs to TUCS Research Unit(s): Learning and Reasoning Lab, Software Construction Laboratorium

Publication Forum rating of this publication: level 2

Edit publication