Abstract
We extend Hoare's 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.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Clarke, E.M.: Programming language constructs for wich it is impossible to obtain good Hoare-like axioms. JACM 26, 129–147, 1979
Clarke, E.M., German, S.M. and Halpern, J.Y.: Reasoning about procedures as parameters. Proc. of the CMU Workshop on Logics of Programs, LNCS 164, 206–220, 1983
Cook, S.A.: Soundness and completeness of an axiom system for program verification. SIAM Journ. on Comp. 7, 70–90, 1978
de Bakker, J.W.: Mathematical theory of program correctness. Prentice-Hall, 1980
Damm, W. and Josko, B.: A sound and relatively* complete Hoare-logic for a language with higher type procedures. Acta Informatica 20, 59–102, 1983
Goguen, J.A., Thatcher, J.W., Wagner, E.G. and Wright, J.B.: Initial algebra semantics and continuous algebras. JACM 24, 68–95, 1977
Halpern, J.Y.: A good Hoare axiom system for an ALGOL-like language. Poc. 11th POPL Conf., 262–271, 1983
Harel, D.: First order dynamic logic, LNCS 68, Springer-Verlag, 1979
Halpern, J.Y., Meyer, A.R. and Trakhtenbrot, B.A.: The semantics of local storage, or what makes the free-list free? Proc. 11th POPL Conf., 245–257, 1983
Langmaack, H.: Aspects of programs with finite modes. Proc. of the FCT-Conference, LNCS 158, 241–254, 1983
Manna, Z.: Mathematical theory of computation. McGraw-Hill, 1974
Olderog, E.R.: Sound and complete Hoare-like calculi based on copy rules. Acta Informatica 16, 161–197, 1981
Olderog, E.R.: A characterization of Hoare's logic for programs with PASCAL-like procedures. Proc. 15th ACM Symp. on Theory of Computing, 320–329, 1983
Olderog, E.R.: Correctness of programs with PASCAL-like procedures without global variables. TCS 30, 49–90, 1984
Reynolds, J.C.: The craft of programming. Prentice-Hall International Series in Comp. Sc. 1981
Reynolds, J.C.: Idealized ALGOL. Tools and notions for program construction. D. Néel ed., Cambridge University Press, 121–161, 1982
Sieber, K.: A new Hoare-calculus for programs with recursive parameterless procedures. Bericht A 81/02, Universität Saarbrücken, 1981
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1985 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sieber, K. (1985). A partial correctness logic for procedures. In: Parikh, R. (eds) Logics of Programs. Logic of Programs 1985. Lecture Notes in Computer Science, vol 193. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-15648-8_25
Download citation
DOI: https://doi.org/10.1007/3-540-15648-8_25
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-15648-2
Online ISBN: 978-3-540-39527-0
eBook Packages: Springer Book Archive