Correctness of programs with Pascal-like procedures without global variables

AbstractWe study a programming language LPas consisting of blockstructured programs with a Pascal-like procedure concept which allows procedures as parameters. Due to Clarke (1979) there cannot be any sound and relatively complete Hoare-like system proving partial correctness for the full language LPas. However, in Langmaack and Olderog (1980) it has been conjectured that such a system exists once global variables are disallowed.In this paper we prove a slightly weaker version of this conjecture by presenting a Hoare-like system which is sound and g-complete for all programs in LPas without global variables; g-completeness means completeness modulo a special second-order theory and an appropriate notion of expressiveness. The proof system provides new methods of dealing with procedures which are formalized in the Rule of Separation for procedure calls. The completeness proof for the system is carried out in a transparent way using modified formal computation trees. An example shows how to apply the proposed methods