Swipe to navigate through the chapters of this book
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.
Please log in to get access to this content
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) MATH
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. ACM 52(10), 30–32 (2009) CrossRef
Loeckx, J., Sieber, K.: The Foundations of Program Verification, 2nd edn. Wiley, New York (1987) MATH
Winskel, G.: The Formal Semantics of Programming Languages: An Introduction. Foundations of Computing. MIT Press, Cambridge (1993) MATH
- Hoare Logic
Dr. José Bacelar Almeida
Dr. Maria João Frade
Dr. Jorge Sousa Pinto
Dr. Simão Melo de Sousa
- Springer London
- Sequence number
- Chapter number
- Chapter 5