Comparing Weakest Precondition and Weakest Liberal Precondition
Andrew E. Santosa
School of Computing, National University of Singapore

arXiv:1512.04013v1 [] 13 Dec 2015

Abstract
In this article we investigate the relationships between the classical notions of weakest precondition and
weakest liberal precondition, and provide several results, namely that in general, weakest liberal precondition is neither stronger nor weaker than weakest precondition, however, given a deterministic and
terminating sequential while program and a postcondition, they are equivalent. Hence, in such situation,
it does not matter which definition is used.
Keywords: programming languages, program verification, program analysis, symbolic execution

1. Introduction
Recent years have seen the prevalent usage of symbolic execution [1] for program analysis. Typical
symbolic execution system builds path conditions corresponding to execution paths. A path condition
is a constraint that represents logical relation between the input and output of an execution path. Its
components are constraints modeling the input and output relations of each program statement along the
execution path. A path condition can be used to determine the set of inputs that causes a program to reach
an error state. For example, given an array index i and array size bound s, the path condition represents
the conditions on the input variables that makes array bounds violation i ≥ s holding after executing
a path. A constraint solver can be used to compute an actual program inputs that causes the violation.
There are two well-known notions of the set of inputs represented by a path and violation conditions:
weakest precondition and weakest liberal precondition. These notions are elements of the general notion
of predicate transformation introduced in [2]. Whereas weakest and weakest liberal preconditions computes input conditions in a “backward” manner, in the literature, the notion of predicate transformation
also includes a “forward” transformation called strongest postcondition.
In this article, we explain how weakest and weakest liberal preconditions are different. We also
explain how that under a very common condition of deterministic and terminating programs they are
equivalent. In Section 2 we provide some preliminary definitions together with our first result that in
general, weakest and weakest liberal preconditions are not equivalent. We also present their relationships
when the program is deterministic, and when the program induces a satisfiable transition relation. In
Section 3 we show that given a deterministic and terminating while program, weakest and weakest liberal
preconditions are the same, and in Section 4 we show how to define weakest liberal precondition in terms
of weakest precondition, and in Section 5 we make some concluding remarks.
2. Weakest and Weakest Liberal are Not Equivalent
Here we clarify some terminologies. In this article, we adopt the more common definition of weakest
liberal precondition as in [3]. However, in some literature [4], weakest liberal precondition is instead
termed weakest precondition. Our definition of weakest liberal precondition is equivalent to the weakest
precondition of [4]. On the other hand, weakest precondition that we mean in this article is that of [2]

or [3] which is also sometimes also termed pre-image in the literature (cf. the backward CTL decision
procedure in [5]). Compared to weakest liberal precondition, the notion of weakest precondition as in [3]
and [2] adds the requirement that the precondition should guarantee the termination of the execution.
We now start with some formal definitions. We denote by x̃ a sequence x0 , . . . , xn of (program)
variables with some unspecified n. We abuse the notion of program to also mean any of its fragments
such as, e.g., a statement is also a program. Now, any program P induces a transition relation ρP ( x̃, x̃′ ) on
free variables x̃ and x̃′ , where x̃ represents the program variables before the transition and x̃′ represents
the program variables after the transition. For example, an assignment statement x̃ := f ( x̃) induces the
transition relation x̃′ = f ( x̃). In general, for any condition ϕ, we write ϕ( x̃) to clarify that x̃ and no other
are the free variables in ϕ. Given a program P and a postcondition ϕ( x̃), the weakest liberal precondition
of ϕ( x̃) wrt. P, written wlp(P, ϕ( x̃)), is the formula
∀ x̃′ : ρP ( x̃, x̃′ ) → ϕ( x̃′ )
where ϕ( x̃′ ) is ϕ( x̃) with all its free variables renamed to their primed versions. On the other hand, the
weakest precondition of ϕ( x̃) wrt. P, written wp(P, ϕ( x̃)), is the formula
∃ x̃′ : ρP ( x̃, x̃′ ) ∧ ϕ( x̃′ )
We remove the subscript P from the transition relation symbol whenever it is clear from the context.
Weakest liberal precondition and weakest precondition are not equivalent in general, as stated in the
following theorem.
Theorem 1. In general, weakest liberal precondition is neither stronger nor weaker than weakest precondition.
Proof. If weakest precondition was stronger than weakest liberal precondition, then the following would
be unsatisfiable:
(∃ x̃′ : ρ( x̃, x̃′ ) ∧ ϕ( x̃′ )) ∧ ¬(∀ x̃′ : ρ( x̃, x̃′ ) → ϕ( x̃′ )).
This is equivalent to:
(∃ x̃′ : ρ( x̃, x̃′ ) ∧ ϕ( x̃′ )) ∧ (∃ x̃′ : ρ( x̃, x̃′ ) ∧ ¬ϕ( x̃′ )).
There exists some ρ such that this formula is satisfiable, that is, in case ρ comes from nondeterministic
statement. For example, when ρ( x̃, x̃′ ) is just a satisfiable constraint ϕ( x̃), which says nothing about
x̃′ . More concrete example is when ρ( x̃, x̃′ ) comes from the statements c=read(); or c=rand(seed);
assuming the read() and rand(seed) can return any value.
On the other hand, if weakest liberal precondition was stronger than weakest precondition, then the
following would be unsatisfiable:
(∀ x̃′ : ρ( x̃, x̃′ ) → ϕ( x̃′ )) ∧ ¬(∃ x̃′ : ρ( x̃, x̃′ ) ∧ ϕ( x̃′ )).
This is equivalent to:
(∀ x̃′ : ρ( x̃, x̃′ ) → ϕ( x̃′ )) ∧ (∀ x̃′ : ρ( x̃, x̃′ ) → ¬ϕ( x̃′ )).
However, also in this case there is some ρ such that the formula is satisfiable, that is, when ρ is false.
A concrete example of such ρ is an exit(0); statement in C, or any other statement that aborts the
program.
3. Equivalence of Weakest and Weakest Liberal for Deterministic and Terminating While Programs
Theorem 2. When the transition relation is deterministic, weakest precondition is stronger than weakest
liberal precondition.
2

Proof. We can infer this from the proof of Theorem 1 above. More formally, we show this by proving
that the following is unsatisfiable when ρ( x̃, x̃′ ) is x̃′ = f ( x̃) for some deterministic function f :
(∃ x̃′ : ρ( x̃, x̃′ ) ∧ ϕ( x̃′ )) ∧ ¬(∀ x̃′ : ρ( x̃, x̃′ ) → ϕ( x̃′ )).
This is equivalent to:
(∃ x̃′ : ρ( x̃, x̃′ ) ∧ ϕ( x̃′ )) ∧ (∃ x̃′ : ρ( x̃, x̃′ ) ∧ ¬ϕ( x̃′ )).
Substituting ρ( x̃, x̃′ ) with x̃′ = f ( x̃) we have: ϕ( f ( x̃))∧¬ϕ( f ( x̃)), which is unsatisfiable if f is deterministic.
Theorem 3. When the transition relation is satisfiable, weakest liberal precondition is stronger than
weakest precondition.
Proof. We can infer this from the proof of Theorem 1 above. More formally, we proceed by showing a
contradiction that
wlp(P, ϕ( x̃)) 9 wp(P, ϕ( x̃))
(1)
is unsatisfiable in case ρ( x̃, x̃′ ) is satisfiable. It is easy to see that (1) is equivalent to:
∀ x̃′ : ρ( x̃, x̃′ ) → (ϕ( x̃′ ) ∧ ¬ϕ( x̃′ ))
which is absurd as ϕ( x̃′ ) ∧ ¬ϕ( x̃′ ) is false and ρ( x̃, x̃′ ) 9 false.
In the special case of sequential programs, since the weakest liberal precondition is actually equivalent
to weakest precondition. Following is the proof why, for sequential programs, weakest liberal precondition is equivalent to weakest precondition.
Definition 1. A deterministic sequential while program may contain assignments, if conditionals, and
while loops, and their sequential compositions in the usual manner. In addition, for any assignment
x̃ := f ( x̃), f is a deterministic function.
Let us now examine the transition relation induced by each of the statement of a deterministic sequential while program:
1. For an assignment x̃ := f ( x̃), the transition relation ρ( x̃, x̃′ ) is x̃′ = f ( x̃).
2. For an if conditional
if ϕ( x̃) then P else P′
when the transition relation for P is ρP ( x̃, x̃′ ) and the transition relation for P′ is ρP′ ( x̃, x̃′ ), the
transition relation ρ( x̃, x̃′ ) induced by the if conditional is
(ϕ( x̃) ∧ ρP ( x̃, x̃′ )) ∨ (¬ϕ( x̃) ∧ ρP′ ( x̃, x̃′ ))
3. For a while loop
while ϕ( x̃) do P
when the transition relation for P is ρP ( x̃, x̃′ ), then the transition relation for the while loop is the
infinite formula
(¬ϕ( x̃) ∧ x̃′ = x̃)∨
(ϕ( x̃) ∧ ρP ( x̃, x̃1 ) ∧ ¬ϕ( x̃1 ) ∧ x̃′ = x̃1 )∨
(ϕ( x̃) ∧ ρP ( x̃, x̃1 ) ∧ ϕ( x̃1 ) ∧ ρP ( x̃1 , x̃2 ) ∧ ¬ϕ( x̃2 ) ∧ x̃′ = x̃2 )∨
V
. . . (ϕ( x̃) ∧ ρP ( x̃, x̃1 ) ∧ ( ni=2 : ϕ( x̃i−1 ) ∧ ρP ( x̃i−1 , x̃i )) ∧ ¬ϕ( x̃n ) ∧ x̃′ = x̃n )∨
...
3

or,

∞
i−1
_
^
(∃ x̃0 , . . . , x̃i : ( (ϕ( x̃ j ) ∧ ρP ( x̃ j , x̃ j+1 )) ∧ ¬ϕ( x̃i ) ∧ x̃′ = x̃i ∧ x̃ = x̃0 ))
i=0

j=0

It is important to note here that for any nonterminating program P, ¬ϕ( x̃i ) for all i is unsatisfiable,
hence ρP ( x̃, x̃′ ) is false.
Note that a deterministic while program induces a transition relation that is always satisfiable, since
if and while conditionals construct two guarded program paths which guards are opposite of each other.
Hence, given a program execution state, both guards cannot be unsatisfiable. Since a deterministic while
program is both deterministic and has transition relation that is always satisfiable, Theorems 2 and 3
seem to have already suggested that a deterministic while program would have equivalent weakest liberal
precondition and weakest precondition, however, here we will proceed more formally and carefully.
Lemma 1. The weakest liberal precondition of an assignment is equivalent to its weakest precondition.
Proof. Given an assignment x̃ := f ( x̃) and a postcondition ϕ( x̃), the weakest liberal precondition is
∀ x̃′ : x̃′ = f ( x̃) → ϕ( x̃′ )
and the weakest precondition is
∃ x̃′ : x̃′ = f ( x̃) ∧ ϕ( x̃′ ),
each one is equivalent to ϕ( f ( x̃)), given f deterministic function.
Lemma 2. When for each program P and P′ , the weakest liberal precondition is equivalent to the weakest
precondition given any postcondition, then given a postcondition ϕ( x̃), the sequence PP′ has equivalent
weakest liberal precondition and weakest precondition.
Proof. Given the postcondition ϕ( x̃), the weakest liberal precondition of of ϕ(x) wrt. P′ is PreP′ , which
is necessarily equivalent to the weakest precondition of ϕ(x) wrt. P′ . Now, given PreP′ as postcondition,
the weakest liberal precondition and weakest precondition of PreP′ wrt. P are necessarily equivalent from
our assumption that for any postcondition ϕ and program P, wlp(P, ϕ) ≡ wp(P′ , ϕ).
Theorem 4. Given a deterministic and terminating sequential while program P and a postcondition, the
weakest liberal precondition of the program wrt. the postcondition is equivalent to the weakest precondition of the program wrt. the postcondition.
Proof. We prove inductively. When P is just a sequence of assignments, from Lemma 1 and Lemma 2
we obtain the desired result.
Now let us assume P to be an if conditional, say of the form
if ϕ( x̃) then P else P′
As our induction hypothesis, we also assume that both P and P′ have equivalent weakest liberal precondition and weakest precondition given any postcondition. Now suppose that the postcondition of the
statement is ϕ. Recall that the transition relation of an if conditional is
(ϕ( x̃) ∧ ρP ( x̃, x̃′ )) ∨ (¬ϕ( x̃) ∧ ρP′ ( x̃, x̃′ ))
The weakest liberal precondition of the if condition, given ϕ as postcondition is therefore
(∀ x̃′ : ((ϕ( x̃) ∧ ρP ( x̃, x̃′ )) ∨ (¬ϕ( x̃) ∧ ρP′ ( x̃, x̃′ ))) → ϕ( x̃′ ))

4

which is equivalent to
(ϕ( x̃) → (∀ x̃′ : ρP ( x̃, x̃′ ) → ϕ( x̃′ ))) ∧ (¬ϕ( x̃) → (∀ x̃′ : ρP′ ( x̃, x̃′ ) → ϕ( x̃′ )))
Note that in the above,
∀ x̃′ : ρP ( x̃, x̃′ ) → ϕ( x̃′ )
and
∀ x̃′ : ρP′ ( x̃, x̃′ ) → ϕ( x̃′ )
are the weakest liberal preconditions of ϕ( x̃) wrt. respectively P and P′ . We name them PreP ( x̃) and
PreP′ ( x̃), respectively, obtaining (2) below:
(ϕ( x̃) → PreP ( x̃)) ∧ (¬ϕ( x̃) → PreP′ ( x̃))

(2)

Now the weakest precondition of ϕ wrt. the if condition, is:
(∃ x̃′ : (ϕ( x̃) ∧ ρP ( x̃, x̃′ )) ∨ (¬ϕ( x̃) ∧ ρP′ ( x̃, x̃′ )) ∧ ϕ( x̃′ ))
which is equivalent to
(ϕ( x̃) ∧ (∃ x̃′ : ρP ( x̃, x̃′ ) ∧ ϕ( x̃′ ))) ∨ (¬ϕ( x̃) ∧ (∃ x̃′ : ρP′ ( x̃, x̃) ∧ ϕ( x̃′ )))
Since the weakest precondition and weakest liberal preconditions of P and P′ are equivalent, we get:
(ϕ( x̃) ∧ PreP ( x̃)) ∨ (¬ϕ( x̃) ∧ PreP′ ( x̃))
This is equivalent to (2).
While loop of the syntax
while ϕ( x̃) do P
has the same semantics as the following infinite program consisting of if conditionals.
if ϕ( x̃) then
P
if ϕ( x̃) then
P
...
The infinite programs exactly induces the same transition relation as the while loop presented above.
Due to termination assumption, the same while loop can be written using a finite number of if conditionals (from the first if conditional up to the last (innermost) if conditional where ϕ( x̃) is false). More
importantly, the while loop induces a transition relation that is satisfiable (not false), that is, there is a
possible execution from the point before the loop to the point right after the loop. Since one if conditional
preserves the equivalence of weakest liberal precondition and weakest precondition, as above, so does
terminating while loops (which are representable as finite number of ifs).
4. Discussion
It is easy to see that the following relationship holds between weakest liberal precondition and weakest
precondition, where the weakest liberal precondition
∀ x̃′ : ρ( x̃, x̃′ ) → ϕ( x̃′ )
5

is actually equivalent to the negation of the weakest precondition of the negated postcondition.
¬(∃ x̃′ : ρ( x̃, x̃′ ) ∧ ¬ϕ( x̃′ )).
This fact has been mentioned by Bourdoncle in his abstract debugging approach [6], where he introduced
two kinds of assertions to be guaranteed by a correctly running programs: always assertions and eventually assertions. The proofs of both require program state-space exploration using backward fixpoint
computations. The state-space exploration of the always assertions employ weakest liberal precondition
while the state-space exploration of the eventually assertions employ weakest precondition. The intuitive
relations between both assertions is that, if suppose that we had an always assertion of some program
correctness condition, and if the assertion holds, then in no circumstance that a program state where that
assertion is violated can be eventually reached. That is, it is not the case that a negation of the correctness
condition eventually holds.
Weakest precondition guarantees the total correctness of a Hoare’s triples {Pre} S {ϕ}, where Pre is
a precondition, ϕ a postcondition, and S a statement. The notion of weakest liberal precondition, on the
other hand, guarantees only partial correctness of the triples, where the postcondition is guaranteed to
hold only when the statement was executed successfully.
As a note, we can define weakest liberal precondition using weakest precondition. This does not mean,
however, that we cannot implement weakest liberal precondition propagation indirectly using weakest
precondition computation. Note that in a sequence PP′ the weakest liberal precondition of a condition
ϕ( x̃) wrt. the program P′ is wlp(ϕ( x̃), P′ ), which is equivalent to ∀ x̃′′ : (ρP′ ( x̃, x̃′′ ) → ϕ( x̃′′ )), where ρP′
is the state transition relation defined by the program P′ . Now, the weakest liberal precondition of the
sequence is
∀ x̃′ : ρP ( x̃, x̃′ ) → (∀ x̃′′ : (ρP′ ( x̃′ , x̃′′ ) → ϕ( x̃′′ )))
which is equivalent to
∀ x̃′ , x̃′′ : (ρP ( x̃, x̃′ ) ∧ ρP′ ( x̃′ , x̃′′ )) → ϕ( x̃′′ ).
Notice that ρP ( x̃, x̃′ ) ∧ ρP′ ( x̃′ , x̃′′ ) is wp(PP′ , true).
5. Concluding Remarks
The semantics of the guarded commands language introduced in [2] embeds the notion of termination.
In [2], weakest precondition has to satisfy an additional condition Q (satisfiability of at least one guard in
case of guarded ifs, and a measure for the termination of a guarded loop), which ensures the termination
of the statement. However, Q does not exclude nondeterminism, and therefore from Theorems 1, 2, and
3, we infer that the notion of weakest precondition and Q in [3] is stronger than the notion of weakest
precondition used in this article.
We note that in this article, we have considered value nondeterminism of functions, while [2] consider
control nondeterminism where multiple guards can be true at the same time and the semantics does not
specify which branch is taken. However, control nondeterminism can always be modeled using value
nondeterminism by having some guards which depend on random value.
[1] J. C. King, Symbolic execution and program testing, Communications of the ACM 19 (7) (1976)
385–394.
[2] E. W. Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, Communications of the ACM 18 (8) (1975) 453–457.
[3] E. W. Dijkstra, A Discipline of Programming, Prentice-Hall Series in Automatic Computation,
Prentice-Hall, 1976.

6

[4] N. Bjørner, A. Browne, Z. Manna, Automatic generation of invariants and intermediate assertions,
Theoretical Computer Science 173 (1) (1997) 49–87.
[5] M. R. A. Huth, M. D. Ryan, Logic in Computer Science: Modelling and Reasoning about Systems,
Cambridge University Press, 2000.
[6] F. Bourdoncle, Abstract debugging of higher-order imperative languages, in: 6th PLDI, ACM Press,
1993, pp. 46–55, sIGPLAN Notices 28(6).

7

