On Hoare logic and Kleene algebra with tests.
We show that Kleene algebra with tests (KAT) subsumes propositional Hoare logic (PHL). Thus the specialized syntax and deductive apparatus of Hoare logic are inessential and can be replaced by simple equational reasoning. In addition, we show that all relationally valid inference rules are derivable in KAT and that deciding the relational validity of such rules is PSPACE-complete.
INTRODUCTION
Hoare logic, introduced by C. A. R. Hoare in 1969 [Hoare 1969], was the first formal
system for the specification and verification of well-structured programs. This
pioneering work initiated the field of program correctness and inspired dozens of
technical articles [Cook 1978; Clarke et al. 1983; Cousot 1990]. For this achievement
among others, Hoare received the Turing Award in 1980.
Hoare logic uses a specialized syntax involving partial correctness assertions
The support of the National Science Foundation under grant CCR-9708915 is gratefully
acknowledged. This paper is a revised and expanded version of [Kozen 1999]. Address:
Department of Computer Science, Cornell University, Ithaca, NY 14853-7501, USA. Email:
Permission to make digital or hard copies of part or all of this work for personal or classroom use is
granted without fee provided that copies are not made or distributed for profit or direct commercial
advantage and that copies show this notice on the first page or initial screen of a display along
with the full citation. Copyrights for components of this work owned by others than ACM must
be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on
servers, to redistribute to lists, or to use any component of this work in other works, requires prior
specific permission and/or a fee. Permissions may be requested from Publications Dept, ACM
Inc., 1515 Broadway, New York, NY 10036 USA, fax +1 (212) 869-0481, or permissions@acm.org.
(PCAs) of the form fbg p fcg and a deductive apparatus consisting of a system
of specialized rules of inference. Under certain conditions, these rules are relatively
complete [Cook 1978]; essentially, the propositional fragment of the logic can be
used to reduce partial correctness assertions to static assertions about the underlying
domain of computation.
In this paper we show that this propositional fragment, which we call propositional
Hoare logic (PHL), is subsumed by Kleene algebra with tests (KAT), an
equational algebraic system introduced in [Kozen 1997]. The reduction transforms
PCAs to ordinary equations and the specialized rules of inference to equational
implications (universal Horn formulas). The transformed rules are all derivable in
KAT by pure equational reasoning. More generally, we show that all Hoare-style
inference rules of the form
(1)
that are valid over relational models are derivable in KAT; this is trivially false for
PHL. We also show that deciding the relational validity of such rules is PSPACE -
complete.
A Kleene algebra with tests is defined simply as a Kleene algebra with an embedded
Boolean subalgebra. Possible interpretations include the various standard
relational and trace-based models used in program semantics, and KAT is complete
for the equational theory of these models [Kozen and Smith 1996]. This work shows
that the reasoning power represented by propositional Hoare logic is captured in a
concise, purely equational system KAT that is complete over various natural classes
of interpretations and whose exact complexity is known. Thus for all practical purposes
KAT can be used in place of the Hoare rules in program correctness proofs.
1.1 Related Work
Equational logic possesses a rich theory and is the subject of numerous papers
and texts [Taylor 1979]. Its power and versatility in program specification and
verification are widely recognized [O'Donnell 1985; Goguen and Malcolm 1996].
The equational nature of Hoare logic has been observed previously. Manes and
Arbib [Manes and Arbib 1986] formulate Hoare logic in partially additive semirings
and categories. The encoding of the PCA fbg p fcg as the equation
observed there. They consider only relational models and the treatment of iteration
is infinitary. Bloom and '
Esik [Bloom and '
Esik 1991] reduce Hoare logic to the
equational logic of iteration theories. They do not restrict their attention to while
programs but capture all flowchart schemes, requiring extra notation for insertion,
tupling, and projection. Their development is done in the framework of category
theory. Semantic models consist of morphisms in algebraic theories, a particular
kind of category. Other related work can be found in [Bloom and '
Esik 1992; Main
and Black 1990].
The encoding of the while programming constructs using the regular operators
and tests originated with propositional dynamic logic (PDL) [Fischer and Ladner
1979]. Although strictly less expressive than PDL, KAT has a number of advantages:
(i) it isolates the equational part of PDL, allowing program equivalence proofs to be
expressed in their natural form; (ii) it conveniently overloads the operators +; \Delta; 0; 1,
On Hoare Logic and Kleene Algebra with Tests \Delta 3
allowing concise and elegant algebraic proofs; (iii) it is PSPACE-complete [Cohen
et al. 1996], whereas PDL is EXPTIME-complete [Fischer and Ladner 1979]; (iv)
interpretations are not restricted to relational models, but may be any algebraic
structure satisfying the axioms; and (v) it admits various general and useful algebraic
constructions such as the formation of algebras of matrices over a KAT, which
among other things allows a natural encoding of automata.
Halpern and Reif [Halpern and Reif 1983] prove PSPACE-completeness of strict
deterministic PDL, but neither the upper nor the lower bound of our PSPACE -
completeness result follows from theirs. Not only are PDL semantics restricted
to relational models, but the arguments of [Halpern and Reif 1983] depend on an
additional nonalgebraic restriction: the relations interpreting atomic programs must
be single-valued. Without this restriction, even if only while programs are allowed,
PDL is exponential time hard. In contrast, KAT imposes no such restrictions.
In Section 2 we review the definitions of Hoare logic and Kleene algebra with
tests. In Section 3 we reduce PHL to KAT and derive the Hoare rules as theorems
of KAT. In Section 4 we strengthen this result to show that KAT is complete for
relationally valid rules of the form (1). In Section 5 we prove that the problem of
deciding the relational validity of such rules is PSPACE-complete.
2. PRELIMINARY DEFINITIONS
2.1 Hoare Logic
Hoare logic is a system for reasoning inductively about well-structured programs.
A comprehensive introduction can be found in [Cousot 1990].
A common choice of programming language in Hoare logic is the language of
while programs. The first-order version of this language contains a simple assignment
x := e, conditional test if b then p else q, sequential composition
a looping construct while b do p.
The basic assertion of Hoare logic is the partial correctness assertion (PCA)
where b and c are formulas and p is a program. Intuitively, this statement asserts
that whenever b holds before the execution of the program p, then if and when p
halts, c is guaranteed to hold of the output state. It does not assert that p must
halt.
Semantically, programs p in Hoare logic and dynamic logic (DL) are usually interpreted
as binary input/output relations p M on a domain of computation M, and
assertions are interpreted as subsets of M [Cook 1978; Pratt 1978]. The definition of
the relation p M is inductive on the structure of p; for example, (p
the ordinary relational composition of the relations corresponding to p and q. The
meaning of the PCA (2) is the same as the meaning of the DL formula b ! [p]c,
where ! is ordinary propositional implication and the modal construct [p]c is interpreted
in the model M as the set of states s such that for all (s; the
output state t satisfies c.
Hoare logic provides a system of specialized rules for deriving valid PCAs, one
rule for each programming construct. The verification process is inductive on the
structure of programs. The traditional Hoare inference rules are:
Assignment rule.
Composition rule.
Conditional rule.
fcg if b then p else q fdg
While rule.
fcg while b do p f:b - cg
Weakening rule.
Propositional Hoare logic (PHL) consists of atomic proposition and program sym-
bols, the usual propositional connectives, while program constructs, and PCAs
built from these. Atomic programs are interpreted as binary relations on a set M
and atomic propositions are interpreted as subsets of M. The deduction system of
PHL consists of the composition, conditional, while, and weakening rules (4)-(7)
and propositional logic. The assignment rule (3) is omitted, since there is no first-order
relational structure over which to interpret program variables; in practice, its
role is played by PCAs over atomic programs that are postulated as assumptions.
In PHL, we are concerned with the problem of determining the validity of rules
of the form
over relational interpretations. The premises fb i take the place of the
assignment rule (3) and are an essential part of the formulation.
2.2 Kleene Algebra
Kleene algebra (KA) is the algebra of regular expressions [Kleene 1956; Conway
1971]. The axiomatization used here is from [Kozen 1994]. A Kleene algebra is an
algebraic structure (K; +; \Delta;   ; 0; 1) that is an idempotent semiring under +; \Delta; 0; 1
satisfying
where - refers to the natural partial order on K:
On Hoare Logic and Kleene Algebra with Tests \Delta 5
The operation + gives the supremum with respect to the natural order -. Instead
of (11) and (12), we might take the equivalent axioms
These axioms say essentially that   behaves like the Kleene asterate operator of
formal language theory or the reflexive transitive closure operator of relational
algebra.
Kleene algebra is a versatile system with many useful interpretations. Standard
models include the family of regular sets over a finite alphabet; the family of binary
relations on a set; and the family of n \Theta n matrices over another Kleene algebra.
Other more unusual interpretations include the min,+ algebra used in shortest
path algorithms and models consisting of convex polyhedra used in computational
geometry [Iwano and Steiglitz 1990].
The following are some typical identities that hold in all Kleene algebras:
(p   q)   p
All the operators are monotone with respect to -. In other words, if p - q, then
pr - qr, rp - rq, r.
The completeness result of [Kozen 1994] says that all true identities between
regular expressions interpreted as regular sets of strings are derivable from the
axioms of Kleene algebra. In other words, the algebra of regular sets of strings over
the finite alphabet \Sigma is the free Kleene algebra on generators \Sigma. The axioms are
also complete for the equational theory of relational models.
See [Kozen 1994] for a more thorough introduction.
2.3 Kleene Algebra with Tests
Kleene algebras with tests (KAT) were introduced in [Kozen 1997] and their theory
further developed in [Kozen and Smith 1996; Cohen et al. 1996]. A Kleene algebra
with tests is just a Kleene algebra with an embedded Boolean subalgebra. That is,
it is a two-sorted structure
such that
-(K; +; \Delta;   ; 0; 1) is a Kleene algebra,
is a Boolean algebra, and
-B ' K.
The Boolean complementation operator is defined only on B. Elements of B are
called tests. The letters p; q; arbitrary elements of K and a; b; c denote
tests.
This deceptively simple definition actually carries a lot of information in a concise
package. The operators +; \Delta; 0; 1 each play two roles: applied to arbitrary elements
6 \Delta D. Kozen
of K, they refer to nondeterministic choice, composition, fail, and skip, respectively;
and applied to tests, they take on the additional meaning of Boolean disjunction,
conjunction, falsity, and truth, respectively. These two usages do not conflict-for
example, sequential testing of b and c is the same as testing their conjunction-and
their coexistence admits considerable economy of expression.
The encoding of the while program constructs is as in PDL [Fischer and Ladner
1979]:
if b then p else q
while b do p
For applications in program verification, the standard interpretation would be a
Kleene algebra of binary relations on a set and the Boolean algebra of subsets of
the identity relation. One could also consider trace models, in which the Kleene
elements are sets of traces (sequences of states) and the Boolean elements are sets
of states (traces of length 0). As with KA, one can form the algebra Mat(K; B; n)
of n \Theta n matrices over a KAT (K; B); the Boolean elements of this structure are the
diagonal matrices over B. There is also a language-theoretic model that plays the
same role in KAT that the regular sets of strings over a finite alphabet play in KA,
namely the family of regular sets of guarded strings over a finite alphabet \Sigma with
guards from a set B. This is the free KAT on generators \Sigma; B; that is, the equational
theory of this structure is exactly the set of all equational consequences of the KAT
axioms. Moreover, KAT is complete for the equational theory of relational models
[Kozen and Smith 1996].
3. KAT AND HOARE LOGIC
In this section we encode Hoare logic in KAT and derive the Hoare composition,
conditional, while, and weakening rules as theorems of KAT. We will strengthen
this result in Section 4 by showing that KAT can derive all relationally valid rules
of the form (8).
The PCA fbg p fcg is encoded in KAT by the equation
Intuitively, this says that the program p with preguard b and postguard c has no
halting execution. An equivalent formulation is
which says intuitively that testing c after executing bp is always redundant.
The equivalence of (22) and (23) can be argued easily in KAT. This equivalence
was previously observed by Manes and Arbib [Manes and Arbib 1986]. Assuming
(22),
c) by the axiom a and Boolean algebra
bpc by (22) and the axiom a
On Hoare Logic and Kleene Algebra with Tests \Delta 7
Conversely, assuming (23),
by associativity and Boolean algebra
by the axiom
The equation (23) is equivalent to the inequality bp - bpc, since the reverse
inequality is a theorem of KAT; it follows immediately from the axiom c - 1 of
Boolean algebra and monotonicity of multiplication.
Using (19)-(21) and (23), the Hoare rules (4)-(7) take the following form:
Composition rule:.
Conditional rule:.
While rule:.
Weakening rule:.
These implications are to be interpreted as universal Horn formulas; that is, the
variables are implicitly universally quantified. To establish the adequacy of the
translation, we show that (24)-(27) encoding the Hoare rules (4)-(7) are theorems
of KAT.
Theorem 3.1. The universal Horn formulas (24)-(27) are theorems of KAT.
Proof. First we derive (24). Assuming the premises
we have
bpcqd by (29)
bpqd by (28).
Thus the implication (24) holds.
For (25), assume the premises
Then
by commutativity of tests
bcqd by (30) and (31)
by commutativity of tests
bq)d by distributivity.
For (26), by trivial simplifications it suffices to show
Assume
By (12) we need only show
But
by (32) and monotonicity
- c(bp)   c by (10).
Finally, for (27), we can rewrite the rule as
which follows immediately from the monotonicity of multiplication.
4. A COMPLETENESS THEOREM
Theorem 3.1 says that for any proof rule of PHL, or more generally, for any rule of
the form
derivable in PHL, the corresponding equational implication (universal Horn formula

is a theorem of KAT. In this section we strengthen this result to show (Corollary
4.2) that all universal Horn formulas of the form
that are relationally valid (true in all relational models) are theorems of KAT; in
other words, KAT is complete for universal Horn formulas of the form (34) over
relational interpretations. This result subsumes Theorem 3.1, since the Hoare rules
are relationally valid. Corollary 4.2 is trivially false for PHL; for example, the rule
On Hoare Logic and Kleene Algebra with Tests \Delta 9
is not derivable, since the Hoare rules only increase the length of programs.
In [Kozen and Smith 1996], based on a technique of Cohen [Cohen 1994] for KA,
we showed that a formula of KAT of the form (34) is valid over all models iff it is
valid over *-continuous models; moreover, its validity over either class of models is
equivalent to the validity of a pure equation. We strengthen this result by showing
that this equivalence still holds when models are further restricted to relational
models. The deductive completeness of KAT over relationally valid formulas of the
form (34) follows as a corollary.
Let T \Sigma;B denote the set of terms of the language of KAT over primitive propositions
and primitive tests g. Let r
. The formula (34) is equivalent
to Consider the four conditions
KAT   ffl
It does not matter whether (38) is preceded by KAT, KAT   , or REL, since the equational
theories of these classes coincide [Kozen and Smith 1996]. It was shown in
[Kozen and Smith 1996] that the metastatements (35), (36), and (38) are equivalent.
We wish to add (37) to this list.
The algebra G \Sigma;B of regular sets of guarded strings over \Sigma; B and the standard
were defined in [Kozen and Smith 1996]. We briefly
review the definitions here. An atom of B is a term of the form c 1
is either b i or b i . An atom represents an atom of the free Boolean algebra generated
by B. Atoms are denoted ff; guarded string over \Sigma; B is a term of the
where each p i 2 \Sigma and each fi i is an atom. This includes the case
are guarded strings. If xff; fiy are guarded strings and product is
xffy. If ff 6= fi, then the product does not exist. We can form the Kleene algebra
of all sets of guarded strings with operations
A
A n
fatoms of Bg:
This becomes a KAT by taking the Boolean algebra of tests to be the powerset
of the set 1. The map G is defined to be the unique homomorphic map on T \Sigma;B
extending
are atoms of Bg; a 2 \Sigma
denotes that b occurs positively in fi. The algebra G \Sigma;B is defined to be
the image of T \Sigma;B under the map G. It was shown in [Kozen and Smith 1996] that
G \Sigma;B is the free KAT on generators \Sigma; B in the sense that for any terms s; t 2 T \Sigma;B ,
Note that G(u) is the set of all guarded strings over \Sigma; B.
Theorem 4.1. The metastatements (35)-(38) are equivalent.
Proof. Since REL ' KAT   ' KAT, the implications
trivially. Also, it is clear that
therefore as well. It thus remains to show that (37) ! (38). Writing
equations as pairs of inequalities, it suffices to show
To show (40), we construct a relational model R on states G(u) \Gamma G(uru). Note
that if x;
then we are done, since in that case G(p) ' G(u) ' G(uru) and the
right-hand side of (40) follows immediately from (39). Similarly, if G(1) ' G(uru),
then G(u) ' G(uuru) ' G(uru) and the same argument applies. We can therefore
assume without loss of generality that both G(u) \Gamma G(uru) and are
nonempty.
The atomic symbols are interpreted in R as follows:
The interpretations of compound expressions are defined inductively in the standard
way for relational models.
We now show that for any t 2 T \Sigma;B ,
by induction on the structure of t. For primitive programs a and tests b,
For the constants 0 and 1, we have
On Hoare Logic and Kleene Algebra with Tests \Delta 11
For compound expressions,
We now show (40). Suppose the left-hand side holds. By (41),
By the left-hand side of (40), R(p) ' R(q). In particular, for any x 2 G(p)\GammaG(uru),
G(uru). But this
It follows from (39) that the right-hand side of (40) holds.
Corollary 4.2. KAT is deductively complete for formulas of the form (34) over
relational models.
Proof. If the formula (34) is valid over relational models, then by Theorem 4.1,
holds. Since KAT is complete for valid equations,
But clearly
therefore
5. COMPLEXITY
As defined in Section 2.1, the decision problem for PHL is to determine whether
a given rule of the form (8) is valid over all relational interpretations. Note that
PSPACE-hardness does not follow immediately from the PSPACE-hardness of the
equational theory, since the conclusion fbg p fcg is of a restricted form
Indeed, E. Cohen has shown [Cohen 1999] that the complexity of valid equations
of the form in KAT is NP-complete.
Theorem 5.1. The decision problem for PHL is PSPACE-complete.
Proof. The reduction of Sections 3 and 4 transforms the decision problem for
PHL to the problem of the universal validity of Horn formulas of the form (34). As
shown in Section 4, this can be reduced to testing the validity of a single equation
without premises. The equational theory of KAT is decidable in PSPACE [Cohen
et al. 1996], thus the decision problem for PHL is in PSPACE.
We now show that the problem is PSPACE-hard. This holds even if the premises
are restricted to refer only to atomic programs, and even if they are
restricted to refer only to a single atomic program p. We give a direct encoding
of the computation of a polynomial space-bounded one-tape deterministic Turing
machine in an instance of the decision problem for PHL. Our approach is similar to
[Halpern and Reif 1983], using the premises fb i to circumvent the determinacy
assumption. E. Cohen [Cohen 1999] has given an alternative hardness proof
using the universality problem for regular expressions.
Consider the computation of a polynomially-space-bounded one-tape deterministic
Turing machine M on some input x of length n. Let N be a polynomial bound
on the amount of space used by M on input x. Let Q be the set of states of M , let
\Gamma be its tape alphabet, let s be its start state, and let t be its unique halt state. We
use polynomially many atomic propositional symbols with the following intuitive
meanings:
th tape cell currently contains symbol a,"
tape head is currently scanning the ith tape cell,"
"the machine is currently in state q," q 2 Q.
Let p be an atomic program. Intuitively, p represents the action of one step of M .
We will devise a set of assumptions OE that will say that faithfully models
the action of M . The PCA / will say that if started in state s on input x, the
program
while the current state is not t do p
fails. The PCA / will be a logical consequence of OE does not halt
on input x.
The start configuration of M on x consists of a left endmarker ' written on tape
cell 0, the input an written on cells 1 through n, and the remainder of
the tape filled with the blank symbol t out to the N th cell. The machine starts in
state s scanning the left endmarker. This situation is captured by the propositional
start
1-i-n
On Hoare Logic and Kleene Algebra with Tests \Delta 13
We will need a formula to ensure that M is in at most one state, that it is
scanning at most one tape cell, and that there is at most one symbol written on
each tape cell:
a6=b
We include the PCA
as one of the assumptions OE i to ensure that format is an invariant of p and therefore
preserved throughout the simulation of M .
Suppose the transition function of M says that when scanning a cell containing
symbol a in state p, M prints the symbol b on that cell, moves right, and enters
state q. We capture this constraint by the family of PCAs
All these PCAs are included for each possible transition of the machine; there are
only polynomially many in all.
We must also ensure that the symbols on tape cells not currently being scanned
do not change; this is accomplished by the family of PCAs
These are the assumptions OE our instance of the decision problem. It
is apparent that under any interpretation of p satisfying these PCAs, successive
executions of p starting from any state satisfying start - format move only to
states whose values for the atomic propositions S q , T i;a , and H i model valid configurations
of M , and the values change in such a way as to model the computation
of M . Thus there is a reachable state satisfying S t iff M halts on x.
We take as our conclusion / the PCA
fstart - formatg while :S t do p ffalseg;
which says intuitively that when started in the start configuration, repeatedly executing
will never cause M to enter state t. The PCA / is therefore a logical
consequence of OE does not halt on x.

ACKNOWLEDGMENTS

I thank Krzysztof Apt, Steve Bloom, Ernie Cohen, Zolt'an '
Esik, Joe Halpern, Greg
Morrisett, Moshe Vardi, and Thomas Yan for valuable comments on an earlier
version of this paper [Kozen 1999].



--R





Hypotheses in Kleene algebra.
Available as ftp://ftp.
Personal communication.
The complexity of Kleene algebra with tests.
Technical Report 96-1598 (July)
Regular Algebra and Finite Machines.
Soundness and completeness of an axiom system for program verification.

Methods and logics for proving programs.
Propositional dynamic logic of regular programs.

Algebraic Semantics of Imperative Programs.
Foundations of Computing.
The propositional dynamic logic of deterministic
An axiomatic basis for computer programming.
A semiring on convex polygons and zero-sum cycle problems
Representation of events in nerve nets and finite automata.
Shannon and J.
A completeness theorem for Kleene algebras and the algebra of regular events.
Kleene algebra with tests.
On Hoare logic and Kleene algebra with tests.
Kleene algebra with tests: Completeness and decidability.

Semantic models for total correctness and fairness.

Algebraic Approaches to Program Semantics.
Equational Logic as a Programming Language.
A practical decision method for propositional dynamic logic.
Theory of Comput.
Equational logic.
--TR
Equational logic as a programming language
Algebraic approaches to program semantics
Semantic models for total correctness and fairness
A semiring on convex polygons and zero-sum cycle problems
Methods and logics for proving programs
Floyd-Hoare logic in iteration theories
A completeness theorem for Kleene algebras and the algebra of regular events
Kleene algebra with tests
Effective Axiomatizations of Hoare Logics
An axiomatic basis for computer programming
Algebraic Semantics of Imperative Programs
Program Correctness and Matricial Iteration Theories
Kleene Algebra with Tests
A practical decision method for propositional dynamic logic (Preliminary Report)
The Complexity of Kleene Algebra with Tests

--CTR
Cohen , Dexter Kozen, A note on the complexity of propositional Hoare logic, ACM Transactions on Computational Logic (TOCL), v.1 n.1, p.171-174, July 2000
Dexter Kozen, Some results in dynamic model theory, Science of Computer Programming, v.51 n.1-2, p.3-22, May 2004
Dexter Kozen , Jerzy Tiuryn, Substructural logic and partial correctness, ACM Transactions on Computational Logic (TOCL), v.4 n.3, p.355-378, July
Bernhard Mller , Georg Struth, Algebras of modal operators and partial correctness, Theoretical Computer Science, v.351 n.2, p.221-239, 21 February 2006
J. von Wright, Towards a refinement algebra, Science of Computer Programming, v.51 n.1-2, p.23-45, May 2004
Jules Desharnais , Bernhard Mller , Georg Struth, Kleene algebra with domain, ACM Transactions on Computational Logic (TOCL), v.7 n.4, p.798-833, October 2006
kleene algebra;hoare logic;dynamic logic;specification;kleene algebra with tests