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.
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\}
where
P
Q
C
P
Q
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.
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.[4] Thus the intuitive reading of a Hoare triple is: Whenever
P
C
Q
C
Q
Q
C
"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:[5]
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.[6]
\dfrac{}{\{P\}tt{skip}\{P\}}
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:
\dfrac{}{\{P[E/x]\}x:=E\{P\}}
where
P[E/x]
The assignment axiom scheme means that the truth of
P[E/x]
P[E/x]
P[E/x]
\negP[E/x]
Examples of valid triples include:
\{x+1=43\}y:=x+1\{y=43\}
\{x+1\leqN\}x:=x+1\{x\leqN\}
All preconditions that are not modified by the expression can be carried over to the postcondition. In the first example, assigning
y:=x+1
x+1=43
y=43
x+1=43
P[(x+1)/y]
x+1=43
x+1=43
x+1=43
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:
\{P\}x:=E\{P[E/x]\}
\{x=5\}x:=3\{3=5\}
Another incorrect rule looking tempting at first glance is
\{P\}x:=E\{P\wedgex=E\}
\{x=5\}x:=x+1\{x=5\wedgex=x+1\}
While a given postcondition uniquely determines the precondition
P[E/x]
\{0\leqy ⋅ y\wedgey ⋅ y\leq9\}x:=y ⋅ y\{0\leqx\wedgex\leq9\}
\{0\leqy ⋅ y\wedgey ⋅ y\leq9\}x:=y ⋅ y\{0\leqx\wedgey ⋅ y\leq9\}
\{0\leqy ⋅ y\wedgey ⋅ y\leq9\}x:=y ⋅ y\{0\leqy ⋅ y\wedgex\leq9\}
\{0\leqy ⋅ y\wedgey ⋅ y\leq9\}x:=y ⋅ y\{0\leqy ⋅ y\wedgey ⋅ y\leq9\}
The assignment axiom proposed by Hoare does not apply when more than one name may refer to the same stored value. For example,
\{y=3\}x:=2\{y=3\}
\{P\}
\{P[2/x]\}
\{y=3\}
S;T
\dfrac{\{P\}S\{Q\} , \{Q\}T\{R\}}{\{P\}S;T\{R\}}
For example, consider the following two instances of the assignment axiom:
\{x+1=43\}y:=x+1\{y=43\}
and
\{y=43\}z:=y\{z=43\}
By the sequencing rule, one concludes:
\{x+1=43\}y:=x+1;z:=y\{z=43\}
Another example is shown in the right box.
\dfrac{\{B\wedgeP\}S\{Q\} , \{\negB\wedgeP\}T\{Q\}}{\{P\}tt{if} B tt{then} S tt{else} T tt{endif}\{Q\}}
The conditional rule states that a postcondition common to and part is also a postcondition of the whole statement.[8] 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
tt{if} B tt{then} S tt{else} T tt{endif}
tt{bool} b:=tt{true};tt{while} B\wedgeb tt{do} S;b:=tt{false} tt{done};b:=tt{true};tt{while} \negB\wedgeb tt{do} T;b:=tt{false} tt{done}
\dfrac{P1 → P2 , \{P2\}S\{Q2\} , Q2 → Q1}{\{P1\}S\{Q1\}}
This rule allows to strengthen the precondition
P2
Q2
For example, a proof of
\{0\leqx\leq15\}tt{if} x<15 tt{then} x:=x+1 tt{else} x:=0 tt{endif}\{0\leqx\leq15\}
\{0\leqx\leq15\wedgex<15\}x:=x+1\{0\leqx\leq15\}
\{0\leqx<15\}x:=x+1\{0\leqx\leq15\}
\{0\leqx\leq15\wedgex\geq15\}x:=0\{0\leqx\leq15\}
\{x=15\}x:=0\{0\leqx\leq15\}
However, the assignment rule for the part requires to choose as
0\leqx\leq15
\{0\leqx+1\leq15\}x:=x+1\{0\leqx\leq15\}
\{-1\leqx<15\}x:=x+1\{0\leqx\leq15\}
\{-1\leqx<15\}
\{0\leqx<15\}
Similarly, for the part, the assignment rule yields
\{0\leq0\leq15\}x:=0\{0\leqx\leq15\}
\{tt{true}\}x:=0\{0\leqx\leq15\}
P1
P2
\{x=15\}
\{tt{true}\}
\{x=15\}
\dfrac{\{P\wedgeB\}S\{P\}}{\{P\}tt{while} B tt{do} S tt{done}\{\negB\wedgeP\}}
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
\negB
For example, a proof of
\{x\leq10\}tt{while} x<10 tt{do} x:=x+1 tt{done}\{\negx<10\wedgex\leq10\}
\{x\leq10\wedgex<10\}x:=x+1\{x\leq10\}
\{x<10\}x:=x+1\{x\leq10\}
\{\negx<10\wedgex\leq10\}
\{x=10\}
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:
\{tt{true}\}tt{while} x ⋅ x ≠ a tt{do} tt{skip} tt{done}\{x ⋅ x=a\wedgett{true}\}
\{tt{true}\wedgex ⋅ x ≠ a\}tt{skip}\{tt{true}\}
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.
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.
\dfrac{< isawell-foundedorderingontheset D , [P\wedgeB\wedget\inD\wedget=z]S[P\wedget\inD\wedget<z]}{[P\wedget\inD]tt{while} B tt{do} S tt{done}[\negB\wedgeP\wedget\inD]}
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
N
Z
R+
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.)
Resuming the first example of the previous section, for a total-correctness proof of
[x\leq10]tt{while} x<10 tt{do} x:=x+1 tt{done}[\negx<10\wedgex\leq10]
10-x
[x\leq10\wedgex<10\wedge10-x\geq0\wedge10-x=z]x:=x+1[x\leq10\wedge10-x\geq0\wedge10-x<z]
10-x
The previous proof goal can be simplified to
[x<10\wedge10-x=z]x:=x+1[x\leq10\wedge10-x<z]
[x+1\leq10\wedge10-x-1<z]x:=x+1[x\leq10\wedge10-x<z]
[x+1\leq10\wedge10-x-1<z]
[x<10\wedge10-x=z]
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.
P\{C\}Q
\{P\}C\{Q\}
\dfrac{\alpha,\beta}{\phi}
\dfrac{}{ \phi }