Programmentwicklung und Verifikation. (Program development and verification.)

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

Gerald Futschek describes formal approaches for program verification; the correspondence of the formal program specification and the formal description of program effects are being verified. In a short introduction the differences between program verification and program testing are shown. With some instructive examples a framework for the program verification is being built up. Based on an outer program specification which consists of the pre- and the postcondition inner program effects are specified in more detail by program invariants and assertions. In this context program assertions are guaranteed properties or states. For the description extended structure charts and a language based on the predicate calculus are used. With the integration of the program variables and the corresponding values interpreted as program states in an abstract space of states one gets a complete model for program specification. This model consists of algorithmic structure charts and simultaneously developed logic elements of specification (pre- , postcondition and assertions). For the real program verification these elements are connected by verification rules for the main structure chart elements sequence, alternative and iteration. The correctness of a program structure is being verified by the correctness of partial structures. By various examples the described method is demonstrated. Finally G. Futschek shows possible extensions concerning subroutines, program inversions and program parallelisms. This book presents a well structured introduction to program verification. By a lot of examples and exercises (with solutions) the software engineer experienced in mathematics and especially in logic is able to use these methods in practice. Some more extensive examples show also the practicability concerning bigger programs. Nevertheless, the question is if these methods are transferable and practicable on large software engineering projects. Furthermore the programming principle of recursion which is a very important and future oriented element of higher programming languages has not being considered.

Recommendations

Cited in

(7)

This page was built for publication: Programmentwicklung und Verifikation. (Program development and verification.)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4692775)