Introduction
Sometimes programs need to be analyzed backward. Starting from a particular program state (or states, as specified by a postcondition), we execute statements backward to obtain the desired precondition. In the literature, there are two ways of doing this, that is, by means of weakest precondition (formally defined in [1], also known as weakest liberal precondition in [2]) or pre-image computation (see the backward CTL decision procedure in [3]).
Given a transition relation R(x,x') on variables x and x', where x represents the program variables before the transition and x' represents the program variables after the transition, and a postcondition Post(x'),
This writeup investigates the difference of both weakest precondition and pre-image.
Weakest Precondition and Pre-Image are not Equivalent in General
The following theorem is an important observation.
Theorem 1. In general, weakest precondition is neither stronger nor weaker than pre-image.
Proof. If pre-image is stronger than weakest precondition, then the following would be unsatisfiable: (∃ x' : R(x,x') ∧ Post(x')) ∧ ⌉ (∀ x' : R(x,x') → Post(x')). This is equivalent to: (∃ x' : R(x,x') ∧ Post(x')) ∧ (∃ x' : R(x,x') ∧ ⌉ Post(x')). There exists some R such that this formula is satisfiable, that is, in case R comes from nondeterministic statement. For example, when R(x,x') is just a satisfiable constraint c(x), which says nothing about x'.
On the other hand, if weakest precondition is stronger than pre-image, then the following would be unsatisfiable: (∀ x' : R(x,x') → Post(x')) ∧ $rceil; (∃ x' : R(x,x') ∧ Post(x')). This is equivalent to: (∀ x' : R(x,x') → Post(x')) ∧ (∀ x' : R(x,x') → ⌉ Post(x')). However, also in this case there is some R such that the formula is satisfiable, that is, when R is "false".
Theorem 2. When the transition relation is deterministic, pre-image is stronger than weakest precondition.
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 R(x,x') is of the form x' = f(x) for some deterministic function f: (∃ x' : R(x,x') ∧ Post(x')) ∧ ⌉ (∀ x' : R(x,x') → Post(x')). This is equivalent to: (∃ x' : R(x,x') ∧ Post(x')) ∧ (∃ x' : R(x,x') ∧ ⌉ Post(x')). Substituting R(x,x') with x'=f(x) we have: Post(f(x)) ∧ ⌉ Post(f(x)), which is unsatisfiable if f is deterministic.
| QED |
Theorem 3. When the transition relation is satisfiable, weakest precondition is stronger than pre-image.
Proof. We can infer this from the proof of Theorem 1 above.
More formally, we show that the following is unsatisfiable in case R(x,x') is satisfiable: (∀ x' : R(x,x') → Post(x')) ∧ ⌉ (∃ x' : R(x,x') ∧ Post(x')). This is equivalent to: (∀ x' : R(x,x') → Post(x')) ∧ (∀ x' : R(x,x') → ⌉ Post(x')). The proof is obvious.
| QED |
Equivalence of Weakest Precondition and Pre-Image for Deterministic While Programs
However, in the special case of sequential programs, since the weakest precondition is actually equivalent to pre-image, the unfolding of sequential program modeled in CLP actually represents weakest precondition. Following is the proof why, for sequential programs, weakest precondition is equivalent to pre-image:
Definition. A deterministic sequential while program may contain assignments, if conditionals, and while loops. In addition, for assignments 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:
(⌉ c(x) ∧ x'=x) ∨
(c(x) ∧ RB(x,x1) ∧ ⌉ c(x1) ∧ x'=x1) ∨
(c(x) ∧ RB(x,x1) ∧ c(x1) ∧ RB(x1,x2) ∧ ⌉ c(x2) ∧ x'=x2) ∨
...
(c(x) ∧ RB(x,x1) ∧ (∧ i=2 to n : c(x[i-1]) ∧ RB(x[i-1],x[i])) ∧ ⌉ c(x[n]) ∧ x'=x[n]) ∨
...
or,
∨ i=0 to infinity (∃ x[0],...,x[i] : (∧ j=0 to i-1 (c(x[j]) ∧ RB(x[j],x[j+1])) ∧ ⌉ c(x[i]) ∧ x'=x[i] ∧ x=x[0]))
It is interesting to note here that for nonterminating programs, ⌉ c(x[i]) for all i is unsatisfiable, hence R(x,x') is "false."
| End of definition. |
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 3 and 4 already suggest that deterministic while program has equivalent weakest precondition and pre-image, however, here we will proceed more formally and carefully.
Lemma 1. The weakest precondition of an assignment is equivalent to its pre-image.
Proof. Given an assignment x:=f(x) and a postcondition Post, the weakest precondition is (∀ x' : x'=f(x) → Post(x')) and the pre-image is (∃ x' : x'=f(x) ∧ Post(x')), each equivalent to Post(f(x)), given f deterministic function.
| QED |
Lemma 2. When for each statement S1 and S2, weakest precondition is equivalent to pre-image given any postcondition, then given a postcondition Post, the sequence S1 S2 has equivalent weakest precondition and pre-image.
Proof. Given the postcondition Post, the weakest precondition of S2 with Post as postcondition is Pre1, which is necessarily equivalent to the pre-image of S2 with Post as postcondition. Now, given Pre1 as postcondition, the weakest precondition and pre-image of S1 are necessarily equivalent.
| QED |
Theorem 4. Given a deterministic sequential while program P and a postcondition, the weakest precondition of the program wrt. the postcondition is equivalent to the pre-image of the program wrt. the precondition.
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
(∀ x' : ((c(x) ∧ RB1(x,x')) ∨ (⌉ c(x) ∧ RB2(x,x'))) → Post(x'))
which is equivalent to
(c(x) → (∀ x' : RB1(x,x') → Post(x'))) ∧ (⌉ c(x) → (∀ x' : RB2(x,x') → Post(x')))
Note that in the above, (∀ x' : RB1(x,x') → Post(x')) and (∀ x' : RB2(x,x') → Post(x')) are respectively the weakest precondition of B1 and B2 wrt. Post. We replace them with Pre1(x) and Pre2(x), respectively, obtaining (1) below:
(c(x) → Pre1(x)) ∧ (⌉ c(x) → Pre2(x))
Now the pre-image of the if condition, given Post as postcondition is:
(∃ x': (c(x) ∧ RB1(x,x')) ∨ (⌉ c(x) ∧ RB2(x,x')) ∧ Post(x'))
which is equivalent to
(c(x) ∧ (∃ x': RB1(x,x') ∧ Post(x'))) ∨ (⌉ c(x) ∧ (∃ x': RB2(x,x') ∧ Post(x')))
Since the pre-images and weakest preconditions of B1 and B2 are equivalent, we get:
(c(x) ∧ Pre1(x)) ∨ (⌉ c(x) ∧ Pre2(x))
This is equivalent to (1).
While loop of the syntax
while c(x) do B
has the same semantics as the following infinite program consisting of if conditionals.
if c(x) then
B
if c(x) then
B
...
if c(x) then
B
The infinite programs exactly induces the same transition relation as the while loop presented above. Since if conditional preserves the equivalence of weakest precondition and pre-image, so does while loops.
| QED |
Computing Weakest Precondition Using Pre-Image Computation
This does not mean that we cannot implement weakest precondition propagation indirectly using pre-image computation. Note that in a sequence t1;t2 the weakest precondition of a condition Cf for the statement t2 is wp(Cf,t2), which is equivalent to ∀(xf) (Rt2(x,xf) → Cf[xf/x]), where Rt2 is the state transition relation defined by the statement t2. Now, weakest precondition of the sequence is
∀(xf1) (Rt1(x,xf1) → (∀(xf) (Rt2(x,xf) → Cf[xf/x]))[x/xf1]),
which is equivalent to
∀(xf1,xf) (Rt1(x,xf1) /\ Rt2(xf1,xf) → Cf[xf/xf1]).
Here, Rt1(x,xf1) /\ Rt2(xf1,xf) are obtainable by pre-image computation, with unconditional initial state (final state of the program).
Acknowledgment
The author would like to thank Joxan Jaffar and Abhik Roychoudhury for various discussions.
References