Rules to verify computer program correctness
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
 formula_1
where formula_2 and formula_3 are "assertions" and formula_4 is a "command". formula_2 is named the "precondition" and formula_3 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 formula_2 holds of the state before the execution of formula_4, then formula_3 will hold afterwards, or formula_4 does not terminate. In the latter case, there is no "after", so formula_3 can be any statement at all. Indeed, one can choose formula_3 to be false to express that formula_4 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:
 ;templatestyles src="Template:Blockquote/styles.css" / ;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 “formula_14” should be interpreted “provided that the program successfully terminates, the properties of its results are described by formula_15.” 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.
 formula_16
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:
 formula_17
where formula_18 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 formula_18 is equivalent to the after-assignment truth of P. Thus were formula_18 true prior to the assignment, by the assignment axiom, then P would be true subsequent to which. Conversely, were formula_18 false (i.e. formula_22 true) prior to the assignment statement, P must then be false afterwards.
Examples of valid triples include:
*formula_23
*formula_24
All preconditions that are not modified by the expression can be carried over to the postcondition. In the first example, assigning formula_25 does not change the fact that formula_26, so both statements may appear in the postcondition. Formally, this result is obtained by applying the axiom schema with P being (formula_27 and formula_26), which yields formula_29 being (formula_26 and formula_26), which can in turn be simplified to the given precondition formula_26.
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: formula_33;
this rule leads to nonsensical examples like:
 formula_34
Another "incorrect" rule looking tempting at first glance is formula_35; it leads to nonsensical examples like:
 formula_36
While a given postcondition P uniquely determines the precondition formula_18, the converse is not true. For example:
*formula_38,
*formula_39,
*formula_40, and
*formula_41
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,
 formula_42
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 formula_43 and formula_44 being formula_45).
Rule of composition.
Hoare's rule of composition applies to sequentially executed programs S and T, where S executes prior to T and is written formula_46 (Q is called the "midcondition"):
formula_47
For example, consider the following two instances of the assignment axiom:
formula_48
and
formula_49
By the sequencing rule, one concludes:
formula_50
Another example is shown in the right box.
formula_51
Conditional rule.
The conditional rule states that a postcondition Q common to then and else part is also a postcondition of the whole if...endif statement.
In the then and the else part, the unnegated and negated condition B can be added to the precondition P, respectively.
The condition, B, must not have side effects.
An example is given in the next section.
This rule was not contained in Hoare's original publication.
However, since a statement 
formula_52
has the same effect as a one-time loop construct
formula_53
the conditional rule can be derived from the other Hoare rules.
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.
formula_54
Consequence rule.
This rule allows to strengthen the precondition formula_55 and/or to weaken the postcondition formula_56.
It is used e.g. to achieve literally identical postconditions for the then and the else part.
For example, a proof of
formula_57
needs to apply the conditional rule, which in turn requires to prove
formula_58,   or simplified 
formula_59
for the then part, and
formula_60,   or simplified 
formula_61
for the else part.
However, the assignment rule for the then part requires to choose P as formula_62; rule application hence yields
formula_63,   which is logically equivalent to
formula_64.
The consequence rule is needed to strengthen the precondition formula_65 obtained from the assignment rule to formula_66 required for the conditional rule.
Similarly, for the else part, the assignment rule yields
formula_67,   or equivalently
formula_68,
hence the consequence rule has to be applied with formula_69 and formula_55 being formula_71 and formula_72, respectively, to strengthen again the precondition. Informally, the effect of the consequence rule is to "forget" that formula_71 is known at the entry of the else part, since the assignment rule used for the else part doesn't need that information.
formula_74
While rule.
Here P is the loop invariant, which is to be preserved by the loop body S.
After the loop is finished, this invariant P still holds, and moreover formula_75 must have caused the loop to end.
As in the conditional rule, B must not have side effects.
For example, a proof of 
formula_76
by the while rule requires to prove
formula_77,   or simplified
formula_78,
which is easily obtained by the assignment rule.
Finally, the postcondition formula_79 can be simplified to formula_80.
For another example, the while rule can be used to formally verify the following strange program to compute the exact square root x of an arbitrary number a—even if x is an integer variable and a is not a square number:
formula_81
After applying the while rule with P being true, it remains to prove
formula_82,
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 x must have contained (by chance) the value of a's square root.
In all other cases, it will not terminate; therefore it is not "totally" correct.
While rule for total correctness.
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 as well as partial correctness. Commonly, square brackets are used here instead of curly braces to indicate the different notion of program correctness.
formula_83
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. Since ; is well-founded, a strictly decreasing chain of members of D can have only finite length, so t cannot keep decreasing forever. (For example, the usual order ; is well-founded on positive integers formula_84, but neither on the integers formula_85 nor on positive real numbers formula_86; 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. (This is one of various notations for total correctness.)
Resuming the first example of the previous section, for a total-correctness proof of
formula_87
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 formula_88, which then in turn requires to prove
formula_89
Informally speaking, we have to prove that the distance formula_90 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
formula_91,
which can be proven as follows:
formula_92 is obtained by the assignment rule, and 
formula_93 can be strengthened to formula_94 by the consequence rule.
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.
Notes.
 ;templatestyles src="Reflist/styles.css" / ;
References.
 ;templatestyles src="Reflist/styles.css" / ;