About cookies on this site Our websites require some cookies to function properly (required). In addition, other cookies may be used with your consent to analyze site usage, improve the user experience and for advertising. For more information, please review your options. By visiting our website, you agree to our processing of information as described in IBM’sprivacy statement. To provide a smooth navigation, your cookie preferences will be shared across the IBM web domains listed here.
Publication
Information and Computation
Review
Reasoning about procedures as parameters in the language L4
Abstract
We provide a sound and relatively complete axiom system for partial correctness assertions in an Algol-like language with procedures passed as parameters, but with no global variables (traditionally known as the language L4). The axiom system allows us to reason syntactically about programs and to construct proofs for assertions about complicated programs from proofs of assertions about their components. Such an axiom system for a language with these features had been sought by a number of researchers, but no previously published solution has been entirely satisfactory. Our axiom system extends the natural style of reasoning used in previous Hoare axiom systems to programs with procedures of higher type. The details of the proof that our axiom system is relatively complete in the sense of Cook may be of independent interest, because we introduce results about expressiveness for programs with higher types that are useful beyond the immediate problem of the language L4. We also prove a new incompleteness result that applies to our logic and to similar Hoare logics. © 1989.