[1] The original ideas were seeded by the work of Robert W. Floyd, who had published a similar system[2] for flowcharts.
A triple describes how the execution of a piece of code changes the state of the computation.
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.
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.
"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:[4] 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.
” should be interpreted “provided that the program successfully terminates, the properties of its results are described by
.” 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.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.
denotes the assertion P in which each free occurrence of x has been replaced by the expression E. The assignment axiom scheme means that the truth of
Examples of valid triples include: All preconditions that are not modified by the expression can be carried over to the postcondition.
Formally, this result is obtained by applying the axiom schema with P being (
; it leads to nonsensical examples like: While a given postcondition P uniquely determines the precondition
For example: 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 x and y refer to the same variable (aliasing), although it is a proper instance of the assignment axiom scheme (with both
[6] In the then and the else part, the unnegated and negated condition B can be added to the precondition P, respectively.
In a similar way, rules for other derived program constructs, like for loop, do...until loop, switch, break, continue can be reduced by program transformation to the rules from Hoare's original paper.
Informally, the effect of the consequence rule is to "forget" that
In fact, the strange program is partially correct: if it happened to terminate, it is certain that x must have contained (by chance) the value of a's square root.
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 t, called the loop variant, whose value strictly decreases with respect to a well-founded relation < on some domain set D during each iteration.
(For example, the usual order < is well-founded on positive integers
; all these sets are meant in the mathematical, not in the computing sense, they are all infinite in particular.)
Given the loop invariant P, the condition B must imply that t is not a minimal element of D, for otherwise the body S could not decrease t any further, i.e. the premise of the rule would be false.
[note 3] 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. D being the non-negative integers with the usual order, and the expression t being
The previous proof goal can be simplified to which can be proven as follows: For the second example of the previous section, of course no expression t can be found that is decreased by the empty loop body, hence termination cannot be proved.