Hoare Logic

  • José Bacelar Almeida
  • Maria João Frade
  • Jorge Sousa Pinto
  • Simão Melo de Sousa
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.


Auxiliary 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.


  1. 1.
    Apt, K.R.: Ten years of Hoare’s logic: A survey—part I. ACM Trans. Program. Lang. Syst.3(4), 431–483 (1981) MATHCrossRefGoogle Scholar
  2. 2.
    Backhouse, R.: Program Construction—Calculating Implementations from Specifications. Wiley, New York (2003) Google Scholar
  3. 3.
    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) Google Scholar
  4. 4.
    Hennessy, M.: The Semantics of Programming Languages. Wiley, New York (1990) MATHGoogle Scholar
  5. 5.
    Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM12, 576–580 (1969) MATHCrossRefGoogle Scholar
  6. 6.
    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) Google Scholar
  7. 7.
    Hoare, C.A.R.: Viewpoint retrospective: An axiomatic basis for computer programming. Commun. ACM52(10), 30–32 (2009) CrossRefGoogle Scholar
  8. 8.
    Jones, C.B.: The early search for tractable ways of reasoning about programs. IEEE Ann. Hist. Comput.25(2), 26–49 (2003) MathSciNetCrossRefGoogle Scholar
  9. 9.
    Kleymann, T.: Hoare logic and auxiliary variables. Form. Asp. Comput.11(5), 541–566 (1999) MATHCrossRefGoogle Scholar
  10. 10.
    Loeckx, J., Sieber, K.: The Foundations of Program Verification, 2nd edn. Wiley, New York (1987) MATHGoogle Scholar
  11. 11.
    Nielson, H.R., Nielson, F.: Semantics with Applications: An Appetizer. Undergraduate Topics in Computer Science. Springer, Berlin (2007) MATHCrossRefGoogle Scholar
  12. 12.
    Reynolds, J.C.: Theories of Programming Languages. Cambridge University Press, Cambridge (1998) MATHCrossRefGoogle Scholar
  13. 13.
    Tennent, R.D.: Specifying Software—A Hands-on Introduction. Cambridge University Press, Cambridge (2002) MATHCrossRefGoogle Scholar
  14. 14.
    Winskel, G.: The Formal Semantics of Programming Languages: An Introduction. Foundations of Computing. MIT Press, Cambridge (1993) MATHGoogle Scholar

Copyright information

© Springer-Verlag London Limited 2011

Authors and Affiliations

  • José Bacelar Almeida
    • 1
  • Maria João Frade
    • 2
  • Jorge Sousa Pinto
    • 1
  • Simão Melo de Sousa
    • 2
  1. 1.Depto. InformáticaUniversidade do MinhoBragaPortugal
  2. 2.Depto. InformáticaUniversidade Beira InteriorCovilhãPortugal

Personalised recommendations