Open main menu

Hoare logic (also known as Floyd–Hoare logic or Hoare rules) is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and logician Tony Hoare, and subsequently refined by Hoare and other researchers.[1] The original ideas were seeded by the work of Robert W. Floyd, who had published a similar system[2] for flowcharts.


Hoare tripleEdit

The central feature of Hoare logic is the Hoare triple. A triple describes how the execution of a piece of code changes the state of the computation. A Hoare triple is of the form


where   and   are assertions and   is a command.[note 1]   is named the precondition and   the postcondition: when the precondition is met, executing the command establishes the postcondition. Assertions are formulae in predicate logic.

Hoare logic provides axioms and inference rules for all the constructs of a simple imperative programming language. In addition to the rules for the simple language in Hoare's original paper, rules for other language constructs have been developed since then by Hoare and many other researchers. There are rules for concurrency, procedures, jumps, and pointers.

Partial and total correctnessEdit

Using standard Hoare logic, only partial correctness can be proven, while termination needs to be proved separately. Thus the intuitive reading of a Hoare triple is: Whenever   holds of the state before the execution of  , then   will hold afterwards, or   does not terminate. In the latter case, there is no "after", so   can be any statement at all. Indeed, one can choose   to be false to express that   does not terminate.

Total correctness can also be proven with an extended version of the While rule.[citation needed]

In his 1969 paper, Hoare used a narrower notion of termination which also entailed absence of any run-time errors: "Failure to terminate may be due to an infinite loop; or it may be due to violation of an implementation-defined limit, for example, the range of numeric operands, the size of storage, or an operating system time limit."[3]


Empty statement axiom schemaEdit

The empty statement rule asserts that the   statement does not change the state of the program, thus whatever holds true before   also holds true afterwards.[note 2]


Assignment axiom schemaEdit

The assignment axiom states that, after the assignment, any predicate that was previously true for the right-hand side of the assignment now holds for the variable. Formally, let   be an assertion in which the variable   is free. Then:


where   denotes the assertion   in which each free occurrence of   has been replaced by the expression  .

The assignment axiom scheme means that the truth of   is equivalent to the after-assignment truth of  . Thus were   true prior to the assignment, by the assignment axiom, then   would be true subsequent to which. Conversely, were   false (i.e.   true) prior to the assignment statement,   must then be false afterwards.

Examples of valid triples include:


All preconditions that are not modified by the expression can be carried over to the postcondition. In the first example, assigning   does not change the fact that  , so both statements may appear in the postcondition. Formally, this result is obtained by applying the axiom schema with   being (  and  ), which yields   being (  and  ), which can in turn be simplified to the given precondition  .

The assignment axiom scheme is equivalent to saying that to find the precondition, first take the post-condition and replace all occurrences of the left-hand side of the assignment with the right-hand side of the assignment. Be careful not to try to do this backwards by following this incorrect way of thinking:  ; this rule leads to nonsensical examples like:


Another incorrect rule looking tempting at first glance is  ; it leads to nonsensical examples like:


While a given postcondition   uniquely determines the precondition  , the converse is not true. For example:

  •  ,
  •   ,
  •   , and

are valid instances of the assignment axiom scheme.

The assignment axiom proposed by Hoare does not apply when more than one name may refer to the same stored value. For example,


is wrong if   and   refer to the same variable (aliasing), although it is a proper instance of the assignment axiom scheme (with both   and   being  ).

Rule of compositionEdit

Hoare's rule of composition applies to sequentially executed programs   and  , where   executes prior to   and is written   (  is called the midcondition):[4]


For example, consider the following two instances of the assignment axiom:




By the sequencing rule, one concludes:


Another example is shown in the right box.

Conditional ruleEdit


The conditional rule states that a postcondition   common to   and   part is also a postcondition of the whole   statement. In the   and the   part, the unnegated and negated condition   can be added to the precondition  , respectively. The condition,  , must not have side effects. An example is given in the next section.

This rule was not contained in Hoare's original publication.[1] However, since a statement


has the same effect as a one-time loop construct


the conditional rule can be derived from the other Hoare rules. In a similar way, rules for other derived program constructs, like   loop,   loop,  ,  ,   can be reduced by program transformation to the rules from Hoare's original paper.

Consequence ruleEdit


This rule allows to strengthen the precondition and/or to weaken the postcondition. It is used e.g. to achieve literally identical postconditions for the   and the   part.

For example, a proof of


needs to apply the conditional rule, which in turn requires to prove

 ,   or simplified

for the   part, and

 ,   or simplified

for the   part.

However, the assignment rule for the   part requires to choose   as  ; rule application hence yields

 ,   which is logically equivalent to

The consequence rule is needed to strengthen the precondition   obtained from the assignment rule to   required for the conditional rule.

Similarly, for the   part, the assignment rule yields

 ,   or equivalently

hence the consequence rule has to be applied with   and   being   and  , respectively, to strengthen again the precondition. Informally, the effect of the consequence rule is to "forget" that \{x=15\} is known at the entry of the   part, since the assignment rule used for the   part doesn't need that information.

While ruleEdit


Here   is the loop invariant, which is to be preserved by the loop body  . After the loop is finished, this invariant   still holds, and moreover   must have caused the loop to end. As in the conditional rule,   must not have side effects.

For example, a proof of


by the while rule requires to prove

 ,   or simplified

which is easily obtained by the assignment rule. Finally, the postcondition   can be simplified to  .

For another example, the while rule can be used to formally verify the following strange program to compute the exact square root   of an arbitrary number  —even if   is an integer variable and   is not a square number:


After applying the while rule with   being  , it remains to prove


which follows from the skip rule and the consequence rule.

In fact, the strange program is partially correct: if it happened to terminate, it is certain that   must have contained (by chance) the value of  's square root. In all other cases, it will not terminate; therefore it is not totally correct.

While rule for total correctnessEdit

If the above ordinary while rule is replaced by the following one, the Hoare calculus can also be used to prove total correctness, i.e. termination[note 3] as well as partial correctness. Commonly, square brackets are used here instead of curly braces to indicate the different notion of program correctness.


In this rule, in addition to maintaining the loop invariant, one also proves termination by way of an expression  , called the loop variant, whose value strictly decreases with respect to a well-founded relation   on some domain set   during each iteration. Since   is well-founded, a strictly decreasing chain of members of   can have only finite length, so   cannot keep decreasing forever. (For example, the usual order   is well-founded on positive integers  , but neither on the integers   nor on positive real numbers  ; all these sets are meant in the mathematical, not in the computing sense, they are all infinite in particular.)

Given the loop invariant  , the condition   must imply that   is not a minimal element of  , for otherwise the body   could not decrease   any further, i.e. the premise of the rule would be false. (This is one of various notations for total correctness.) [note 4]

Resuming the first example of the previous section, for a total-correctness proof of


the while rule for total correctness can be applied with e.g.   being the non-negative integers with the usual order, and the expression   being  , which then in turn requires to prove


Informally speaking, we have to prove that the distance   decreases in every loop cycle, while it always remains non-negative; this process can go on only for a finite number of cycles.

The previous proof goal can be simplified to


which can be proven as follows:

  is obtained by the assignment rule, and
  can be strengthened to   by the consequence rule.

For the second example of the previous section, of course no expression   can be found that is decreased by the empty loop body, hence termination cannot be proved.

See alsoEdit


  1. ^ Hoare originally wrote " " rather than " ".
  2. ^ This article uses a natural deduction style notation for rules. For example,   informally means "If both   and   hold, then also   holds";   and   are called antecedents of the rule,   is called its succedent. A rule without antecedents is called an axiom, and written as  .
  3. ^ "Termination" here is meant in the broader sense that computation will eventually be finished; it does not imply that no limit violation (e.g. zero divide) can stop the program prematurely.
  4. ^ Hoare's 1969 paper didn't provide a total correctness rule; cf. his discussion on p.579 (top left). For example Reynolds' textbook (John C. Reynolds (2009). Theory of Programming Languages. Cambridge University Press.), Sect.3.4, p.64 gives the following version of a total correctness rule:   when   is an integer variable that doesn't occur free in  ,  ,  , or  , and   is an integer expression (Reynolds' variables renamed to fit with this article's settings).


  1. ^ a b Hoare, C. A. R. (October 1969). "An axiomatic basis for computer programming" (PDF). Communications of the ACM. 12 (10): 576–580. doi:10.1145/363235.363259. Archived from the original on 2016-03-04.CS1 maint: BOT: original-url status unknown (link)
  2. ^ R. W. Floyd. "Assigning meanings to programs." Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Vol. 19, pp. 19–31. 1967.
  3. ^ p.579 upper left
  4. ^ Huth, Michael; Ryan, Mark (2004-08-26). Logic in Computer Science (second ed.). CUP. p. 276. ISBN 978-0521543101.

Further readingEdit

External linksEdit

  • KeY-Hoare is a semi-automatic verification system built on top of the KeY theorem prover. It features a Hoare calculus for a simple while language.
  • j-Algo-modul Hoare calculus — A visualisation of the Hoare calculus in the algorithm visualisation program j-Algo