A partial correctness logic for procedures (in an ALGOL-like language)

Abstract

We extend Hoares logic by allowing quantifiers and other logical connectives to be used on the level of Hoare formulas. This leads to a logic in which partial correctness properties of procedures (and not only of statements) can be formulated adequately. In particular it is possible to argue about free procedures, i.e. procedures which are not bound by a declaration but only "specified" semantically. This property of our logic (and of the corresponding calculus) is important from both a practical and a theoretical point of view, namely: -Formal proofs of programs can be written in the style of stepwise refinement. -Procedures on parameter position can be handled adequately, so that some sophisticated programs can be verified, which are beyond the power of other calculi. The logic as well as the calculus are similar to Reynolds specification logic. But there are also some (essential) differences which will be pointed out in this paper.