Top

previous chapter First-Order Logic

next chapter Generating Verification Conditions

Hint

Swipe to navigate through the chapters of this book

2011 | OriginalPaper | Chapter

5. Hoare Logic

Authors: Dr. José Bacelar Almeida, Dr. Maria João Frade, Dr. Jorge Sousa Pinto, Dr. Simão Melo de Sousa

Publisher: Springer London

Published in: Rigorous Software Development

» Get access to the full version

Abstract

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

To get access to this content you need the following product:

Computer Science Explorer

Purchase now

Apt, K.R.: Ten years of Hoare’s logic: A survey—part I. ACM Trans. Program. Lang. Syst. 3(4), 431–483 (1981) MATHCrossRef

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.: An axiomatic basis for computer programming. Commun. ACM 12, 576–580 (1969) MATHCrossRef

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

Jones, C.B.: The early search for tractable ways of reasoning about programs. IEEE Ann. Hist. Comput. 25(2), 26–49 (2003) MathSciNetCrossRef

Kleymann, T.: Hoare logic and auxiliary variables. Form. Asp. Comput. 11(5), 541–566 (1999) MATHCrossRef

10.

Loeckx, J., Sieber, K.: The Foundations of Program Verification, 2nd edn. Wiley, New York (1987) MATH

11.

Nielson, H.R., Nielson, F.: Semantics with Applications: An Appetizer. Undergraduate Topics in Computer Science. Springer, Berlin (2007) MATHCrossRef

12.

Reynolds, J.C.: Theories of Programming Languages. Cambridge University Press, Cambridge (1998) MATHCrossRef

13.

Tennent, R.D.: Specifying Software—A Hands-on Introduction. Cambridge University Press, Cambridge (2002) MATHCrossRef

14.

Winskel, G.: The Formal Semantics of Programming Languages: An Introduction. Foundations of Computing. MIT Press, Cambridge (1993) MATH

Title

Hoare Logic

Book

Rigorous Software Development

Print ISBN: 978-0-85729-017-5

Electronic ISBN: 978-0-85729-018-2

https://doi.org/10.1007/978-0-85729-018-2

DOI

https://doi.org/10.1007/978-0-85729-018-2_5

Authors:

Dr. José Bacelar Almeida
Dr. Maria João Frade
Dr. Jorge Sousa Pinto
Dr. Simão Melo de Sousa

Publisher

Springer London

Sequence number

Chapter number

Chapter 5