nLab Hoare logic

Contents

Contents

Idea

Hoare logic [Hoare (1969)] is a form of formal program verification.

[from Streicher (1993, p.1-2):] In theoretical computer science the issue of correctness of programs has become more and more important over the years. Early approaches to establishing correctness were program verification logics such as Hoare calculi for verifying imperative programs and the method of algebraic specification for specifying modules in functional languages.

Program logics as e.g. the Hoare calculus are oriented towards state-oriented programming languages and provide calculi for deriving correct “Hoare triples”, i.e. expressions of the form {P}S{Q}\{P\}S\{Q\} with the intuitive meaning that whenever the initial state of a program satisfies proposition PP then the execution of the program SS terminates and results in a state satisfying proposition QQ.

Although this method works quite well for “pidgin” programs (i.e. using only assignment, if_then_else and while over a single data type) there are big problems with dealing with procedures, modules and general user defined data types. In general a main drawback is that the world of programs and the world of specifications are conceptually quite different. Of course, this problem is typical for all state-oriented imperative programming languages.

This conceptual gap between programs and their specification has been overcome by the appearance and development of functional programming languages. […] for languages supporting the construction and verification of large modular systems the concept of dependent type is inevitable.

References

The original article:

See also:

The above quote is from:

  • Thomas Streicher, p. 1-2 of: Investigations into Intensional Type Theory, Habilitation Thesis, Darmstadt (1993) [pdf, pdf]

which otherwise is about intensional dependent type theory.

Last revised on February 13, 2023 at 20:12:34. See the history of this page for a list of all contributions to it.