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. The original ideas were seeded by the work of Robert W. Floyd, who had published a similar system for flowcharts.
Hoare triple 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
{ P } C { Q } {\displaystyle \{P\}C\{Q\}}
where P {\displaystyle P} and Q {\displaystyle Q} are assertions and C {\displaystyle C} is a command. P {\displaystyle P} is named the precondition and Q {\displaystyle Q} 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 correctness Using standard Hoare logic, only partial correctness can be proven. Total correctness additionally requires termination, which can be proven separately or with an extended version of the While rule. Thus, the intuitive reading of a Hoare triple is: Whenever P {\displaystyle P} holds of the state before the execution of C {\displaystyle C} , then Q {\displaystyle Q} will hold afterwards, or C {\displaystyle C} does not terminate. In the latter case, there is no "after", so Q {\displaystyle Q} can be any statement at all. Indeed, one can choose Q {\displaystyle Q} to be false to express that C {\displaystyle C} does not terminate. "Termination" here and in the rest of this article is meant in the broader sense that computation will eventually be finished, that is, it implies the absence of infinite loops; it does not imply the absence of implementation limit violations (e.g., division by zero), stopping the program prematurely. In his 1969 paper, Hoare used a narrower notion of termination, which also entailed the absence of implementation limit violations, and expressed his preference for the broader notion of termination as it keeps assertions implementation-independent:
Another deficiency in the axioms and rules quoted above is that they give no basis for a proof that a program successfully terminates. 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. Thus the notation “ P { Q } R {\displaystyle P\{Q\}R} ” should be interpreted “provided that the program successfully terminates, the properties of its results are described by R {\displaystyle R} .” It is fairly easy to adapt the axioms so that they cannot be used to predict the “results” of nonterminating programs; but the actual use of the axioms would now depend on knowledge of many implementation-dependent features, for example, the size and speed of the computer, the range of numbers, and the choice of overflow technique. Apart from proofs of the avoidance of infinite loops, it is probably better to prove the “conditional” correctness of a program and rely on an implementation to give a warning if it has had to abandon execution of the program as a result of violation of an implementation limit.
Rules
Empty statement axiom schema The empty statement rule asserts that the skip statement does not change the state of the program, thus whatever holds true before skip also holds true afterwards.
{ P } skip { P } {\displaystyle {\dfrac {}{\{P\}{\texttt {skip}}\{P\}}}}
Assignment axiom schema 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 P be an assertion in which the variable x is free. Then:
{ P [ E / x ] } x := E { P } {\displaystyle {\dfrac {}{\{P[E/x]\}x:=E\{P\}}}}
… excerpt ends here. Continue reading the full article.
