Part of the
Undergraduate Topics in Computer Science
book series (UTICS)
Hoare logic is the fundamental formalism introduced by C.A.R. Hoare in 1969 for reasoning about the correctness of imperative programs, building on first-order logic. In this chapter we study a program logic which is a variant of Hoare logic for programs containing user-provided annotations.
The logic deals with the notion of correctness vis a vis a specification that consists of a precondition and a postcondition. The correctness of a program with respect to a given specification is asserted by constructing a derivation in the inference system of Hoare logic. While doing so, one must identify an invariant for every loop in the program.
This chapter also discusses the important problem of adaptation of specifications, since it has major implications on the design of practical verification systems based on Hoare logic.
KeywordsAuxiliary Variable Abstract Syntax Program Expression Program Variable Side Condition
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Apt, K.R.: Ten years of Hoare’s logic: A survey—part I. ACM Trans. Program. Lang. Syst.3
(4), 431–483 (1981)
Backhouse, R.: Program Construction—Calculating Implementations from Specifications. Wiley, New York (2003)
Cousot, P.: Methods and logics for proving programs. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics (B), pp. 841–994. Elsevier/MIT Press, Cambridge (1990)
Hennessy, M.: The Semantics of Programming Languages. Wiley, New York (1990)
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM12
, 576–580 (1969)
Hoare, C.A.R.: Procedures and parameters: an axiomatic approach. In: Proceedings of Symposium on Semantics of Algorithmic Languages. Lecture Notes in Mathematics, vol. 188. Springer, Berlin (1971)
Hoare, C.A.R.: Viewpoint retrospective: An axiomatic basis for computer programming. Commun. ACM52
(10), 30–32 (2009)
Jones, C.B.: The early search for tractable ways of reasoning about programs. IEEE Ann. Hist. Comput.25
(2), 26–49 (2003)
Kleymann, T.: Hoare logic and auxiliary variables. Form. Asp. Comput.11
(5), 541–566 (1999)
Loeckx, J., Sieber, K.: The Foundations of Program Verification, 2nd edn. Wiley, New York (1987)
Nielson, H.R., Nielson, F.: Semantics with Applications: An Appetizer. Undergraduate Topics in Computer Science. Springer, Berlin (2007)
Reynolds, J.C.: Theories of Programming Languages. Cambridge University Press, Cambridge (1998)
Tennent, R.D.: Specifying Software—A Hands-on Introduction. Cambridge University Press, Cambridge (2002)
Winskel, G.: The Formal Semantics of Programming Languages: An Introduction. Foundations of Computing. MIT Press, Cambridge (1993)
© Springer-Verlag London Limited 2011