×

zbMATH — the first resource for mathematics

Invariant based programming: Basic approach and teaching experiences. (English) Zbl 1178.68334
Summary: 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.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
SIMPLIFY; Python; Spec#; PVS; JML
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Back R-J (1978) Program construction by situation analysis. Research Report 6, Computing Centre, University of Helsinki, Helsinki
[2] Back R-J (1980) Exception handling with multi-exit statements. In: Hoffmann HJ (eds) 6th Fachtagung Programmiersprachen und Programmentwicklungen, volume 25 of Informatik Fachberichte. Springer, Darmstadt, pp 71–82
[3] Back R-J (1983) Invariant based programs and their correctness. In: Biermann W, Guiho G, Kodratoff Y (eds) Automatic program construction techniques. MacMillan, New York, pp 223–242
[4] Burdy L, Cheon Y, Cok DR, Ernst MD, Kiniry JR, Leavens GT, Rustan K, Leino M, Poll E (2005) An overview of jml tools and applications. Softw Tools Technol Transf 7(3)
[5] Back R-J, Eriksson J, Myreen M (2007) Testing and verifying invariant based programs in the socos environment. In: The international conference on tests and proofs (TAP)
[6] Barnett M, Rustan K, Leino M, Schulte W (2004) The spec-sharp programming system: an overview. In: CASSIS 2004 proceedings
[7] Back R, Myreen M (2005) Tool support for invariant based programming. In: Proceedings of the 12th Asia-Pacific software engineering conference, Taipei, Taiwan December 2005
[8] Dijkstra EW (1968) A constructive approach to the problem of program correctness. BIT 8:174–186 · Zbl 0167.46002
[9] Dijkstra EW (1972) Notes on structured programming. In: Dahl O-J, Hoare CAR, Dijkstra EW (eds) Structured programming. Academic Press, New York
[10] Dijkstra EW (1976) A discipline of programming. Prentice-Hall, New York · Zbl 0368.68005
[11] Fowler M (1999) UML distilled. Addison Wesley, Reading
[12] Harel D (1987) State charts: a visual formalism for complex systems. Sci Comput Program 8:231–274 · Zbl 0637.68010
[13] Hehner E (1979) Do considered od: a contribution to the programming calculus. Acta Informatica 11:287–304 · Zbl 0395.68002
[14] Rustan K, Leino M, Nelson G (1998) An extended static checker for modula-3. In: Proceedings of the 7th international conference on compiler construction, Lecture Notes in Computer Science, vol 1383, pp 302–305
[15] Nelson G (1980) Techniques for program verification. PhD Thesis, Stanford University
[16] Owre S, Shankar N, Rushby J (1992) Pvs: a prototype verification system. In: CADE 11, Saratoga Springs, NY
[17] Reynolds JC (1978) Programming with transition diagrams. In: Gries D (eds) Programming methodology. Springer, Berlin · Zbl 0395.68016
[18] Van Emden MH (1979) Programming with verification conditions. IEEE Trans Softw Eng SE-5 · Zbl 0395.68008
[19] Van Rossum G, Drake FL Jr (2003) The python tutorial–an introduction to python. Network Theory Ltd.,
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.