Introduction

This course material is an introduction to some of the most relevant techniques and methods of proving correctness of programs. The approach is assertional, we take the logical standpoint: specifications are formulated as pairs of sets of program states and we seek the proof for the correctness of programs in a formal logical setting: either by model theoretic reasoning or as a result of a formal derivation in a deduction system.

The first chapter is concerned with the case of while programs, which are the simplified representatives of programs written in an an ALGOL-like programming language. The basic components are constructs for assignment, conditional, composition and a tool for formulating a while loop. We glance through the inevitable notions underlying the theory: those of a state, a formal specification and formulation of correctness statements, together with introducing the concept of operational and denotational program semantics. Then we turn to the axiomatic treatment: a Hoare-logic is defined for the verification of partial and of total correctness of while programs. We treat in some extent the questions of soundness and completeness with respect to these calculi, introducing on the meantime two forms of the Dijkstra predicate transformation semantics.

The second chapter deals with the verification of recursive programs. The simplest case is considered: we deal with parameterless recursive procedures only. The main axiomatic tools: the recursion rule and the adaptation rule are introduced and the underlying fixpoint theory is also treated in some length.

The next three chapters are concerned with the primary notions related to parallel programs. We give an outline of the fundamental concepts: starting from disjoint parallel programs we continue with parallel programs that can communicate via shared variables. In the fifth chapter we discuss some problems of synchronization and some solutions given to them.

The last but one chapter recalls the notions of fixpoint theory, and the course material is concluded with a collection of solved exercises.