Programming Notes – Hoare Triple
Programming language theorist C.A.R. Hoare introduced the notation now known as the Hoare Triple as a way of describing the parts of an activated program statement. The Hoare Triple is an integral part of the concept of an axiomatic programming system of valid Hoare Triples. Given a set of Hoare Triples describing correct programming solutions for fundamental program statements and a set of rules used to derive other correct programming solutions also expressed as Hoare Triples, one could presumably derive a set of correct programs.
In his classic paper, Hoare (1969) describes a triple of the form
P {Q} R
where P is a precondition, {Q} is a program, and R is a result. According to Hoare, a valid triple may be interpreted as:
“If the assertion P is true before initiating the program Q, then the assertion R will be true on completion.”
Hoare describes a set of basic axioms that may be used to derive valid triples:
D0. Axiom of assignment P[x := f] {x := f} P
D1. Rules of consequence
if P {Q} R and R Þ S then P {Q} S
if P {Q} R and S Þ P then S {Q} R
if P {Q1} R1 and R1 {Q2} R then P {Q1;Q2} R
D3. Rule of iteration
if (PÙB) {S} P then P {while B do S} (ØBÙP)
Set-based Hoare Triple
The syntax of the Hoare Triple on these pages follows the original syntax:
P {r) R
However, the meaning of the Hoare Triple on these pages differs from the meaning as expressed in the original paper.
First, the precondition and result are interpreted specifically as sets of program states that share a common condition. Thus, the first and last components of the Hoare Triple are interpreted as sets or points in a state space.
The first component of the Hoare triple is the precondition. The precondition describes a set of program states that satisfy some expression. For example, ‘variable x > 0’ can be a precondition. A set of program states is also called a program state space. A description of a program state space can be found in Program States Part 1.
The second component is the program statement. The program statement has two properties. The program statement may be activated. A(r) is true if the statement has been activated, and false if the statement has not been activated. Activation of a program statement may terminate normally, terminate abnormally, or not terminate. T(r) is true if activation leads to normal termination and false for any other result.
The third component of the Hoare triple is the expected result. Like the precondition, the expected result is a set of program states that satisfy some expression. If activation does not occur, then the precondition remains true. If activation occurs, normal termination leads to a valid program state, and a non-empty result set. The result of non-termination or abnormal termination of an activated program statement is not certain.
The second difference is the interpretation of the Hoare Triple. In the original paper, the Hoare Triple expresses a valid program execution. On these pages, however, the Hoare Triple expresses an activation of a program statement, valid or invalid. When the Hoare Triple is valid, all members of the precondition set and activation of the program statement lead to a member of the result set as the program state. Otherwise, the Hoare Triple is not valid.
The Set of Valid Activations
Activation of a program statement can change the program state in some way. Suppose that p Î P, r Î R. The points p and r represent points in state spaces P and R respectively. Let r be a program statement such that the existence of point p and activation of r leads to point r. The points p and r form an ordered pair in the relation r corresponding to the activation of the program statement r. The relation r forms the set of all valid activation events associated with program statement r. The expression
p r r
describes an instance of valid activations. The precondition and result are points describing program states, and the relation represents the program statement.
Hoare Triple as an Expression
The Hoare Triple
P {r} R
represents the notion that all points and program state space P coupled with activation of program statement r leads to a point in program state space R. A Hoare Triple is not valid if any state in the precondition and activation leads to either nontermination or to a result other than that described by the result set.
Hoare Triple and Weakest Precondition
The third difference between the original Hoare Triple and the Hoare Triple used on these pages involves the relationship between the Hoare Triple and the Weakest Precondition. Hoare did not guarantee termination of an activated program statement in his Hoare Triple, but a valid Hoare Triple used on these pages does guarantee program termination, similar to the weakest precondition model. In fact, the Hoare Triple on these pages is a generalization of the weakest precondition model.
Connecting the Hoare Triple concept to the weakest precondition concept provides the opportunity to express the truth-value of a Hoare Triple with reference to a program state point’s membership in the weakest precondition set.
A Simple Example
For ordinary values of variables a and b, the Hoare Triple
{s|a>b:s} {a := a-b} {s|a>0:s}
is valid, because proper termination is not an issue.
Applying Hoare’s axiom of assignment yields the valid Hoare Triple:
{s|a>0:s}[a:=a-b] {a := a-b} {s|a>0:s}
{s|a-b>0:s} {a := a-b} {s|a>0:s}
{s|a>b:s} {a := a-b} {s|a>0:s}
Is the following Hoare Triple valid?
{s|a>5:s} {a := a-b} {s|a>0:s}
What values of the value of b render invalid instances of the Hoare Triple?
Sets in a Hoare Triple may by the individual points in a state space. Which of the following Hoare Triples are valid?
{<’x’,5>,<’y’,10>} (y := x+y) {<’x’,5>,<’y’,15>}
{<’x’,5>,<’y’,25>} (y := x+y) {<’x’,5>,<’y’,15>}
References:
Dijkstra, Edsgar, 1976, A Discipline of Programming, Englewood Cliffs, NJ: Prentice-Hall
Fejer, Peter and Simovici, Dan A., 1991, Mathematical Foundations of Computer Science, New York, NY: Springer-Verlag
Gries, David and Schneider, Fred B., 1993, A Logical Approach to Discrete Math, New York, NY: Springer-Verlag
Hoare, C. A. R., 1969, An Axiomatic Basis for Computer Programming, Communications of the ACM, Volume 12, Number 10, 576-580, 583