Predicate Transformers

Overview

Define ${Q} S {R}$ as the predicate:

If execution of $S$ is begun in a state satisfying $Q$ , then it is guaranteed to terminate in a finite amount of time in a state satisfying $R$ .

Weakest Precondition

For any command $S$ and predicate $R$ , we define the weakest precondition of $S$ with respect to $R$ , denoted $w p (S, R)$ , as

the set of all states such that execution of $S$ begun in any one of them is guaranteed to terminate in a finite amount of time in a state satisfying $R$ .

Expression ${Q} S {R}$ is equivalent to $Q ⟹ w p (S, R)$ .

Law of the Excluded Miracle

Given any command $S$ , $w p (S, F) = F$ .

Distributivity of Conjunction

Given command $S$ and predicates $Q$ and $R$ ,

w p (S, Q \land R) = w p (S, Q) \land w p (S, R)

Law of Monotonicity

Given command $S$ and predicates $Q$ and $R$ , if $Q ⟹ R$ , then $w p (S, Q) ⟹ w p (S, R)$ .

Distributivity of Disjunction

Given command $S$ and predicates $Q$ and $R$ ,

w p (S, Q) \lor w p (S, R) ⟹ w p (S, Q \lor R)

Strongest Postcondition

For any command $S$ and predicate $Q$ , we define the strongest postcondition of $S$ with respect to $Q$ , denoted $s p (S, Q)$ , as

the state such that execution of $S$ begun in a state satisfying $Q$ is guaranteed to terminate in after a finite amount of time.

Expression ${Q} S {R}$ is equivalent to $s p (S, Q) ⟹ R$ .

Commands

Skip

For any predicate $R$ , $w p (s k i p, R) = R$ .

Abort

For any predicate $R$ , $w p (a b o r t, R) = F$ .

Sequential Composition

Sequential composition is one way of composing larger program segments from smaller segments. Let $S 1$ and $S 2$ be two commands. Then $S 1; S 2$ is defined as

w p (^{″} S 1; S 2^{″}, R) = w p (S 1, w p (S 2, R))

Assignment

Simple

The assignment command has form $x : = e$ , provided the types of $x$ and $e$ are the same. This command is read as " $x$ becomes $e$ " and is defined as

w p (^{″} x : = e^{″}, R) = d o m a i n (e) cand R_{e}^{x}

where $d o m a i n (e)$ is a predicate that describes the set of all states in which $e$ may be evaluated.

General

The multiple assignment command has form

x_{1} \circ s_{1}, \dots, x_{n} \circ s_{n} : = e_{1}, \dots, e_{n}

where each $x_{i}$ is an identifier, each $s_{i}$ is a selector, and each expression $e_{i}$ has the same type as $x_{i} \circ s_{i}$ . We denote this assignment more compactly as $\bar{x} : = \bar{e}$ . We define multiple assignment as

w p (^{″} \bar{x} : = {\bar{e}}^{″}, R) = d o m a i n (\bar{e}) cand R_{\bar{e}}^{\bar{x}}

Alternative

The general form of the alternative command is:

\begin{aligned} if & B_{1} \to S_{1} \\ | & B_{2} \to S_{2} \\ \dots \\ | & B_{n} \to S_{n} \\ fi \end{aligned}

Each $B_{i} \to S_{i}$ is called a guarded command. To execute the alternative command, find one true guard and execute the corresponding command. Notice this is nondeterministic. We denote the alternative command as $IF$ and define $IF$ in terms of $w p$ as:

\begin{aligned} w p (IF, R) = & (\forall i, 1 \leq i \leq n ⟹ d o m a i n (B_{i})) \land \\ (\exists i, 1 \leq i \leq n \land B_{i}) \land \\ (\forall i, 1 \leq i \leq n ⟹ (B_{i} ⟹ w p (S_{i}, R))) \end{aligned}

Iterative

The general form of the iterative command is:

\begin{aligned} do & B_{1} \to S_{1} \\ | & B_{2} \to S_{2} \\ \dots \\ | & B_{n} \to S_{n} \\ od \end{aligned}

We denote the iterative command as $DO$ and define $DO$ in terms of $w p$ as:

w p (DO, R) = \exists k \geq 0, H_{k} (R)

where $H_{k}$ is given recursive definition:

\begin{aligned} H_{0} (R) & = \neg (B_{1} \lor \dots \lor B_{n}) \land R \\ H_{k + 1} (R) & = H_{0} (R) \lor w p (IF, H_{k} (R)) \end{aligned}

Bound Functions

A bound function $t$ returns an upper bound on the number of iterations an iterative command may perform. On every iteration, it must evaluate to a smaller number than in the previous iteration. That is, $t (k^{+}) < t (k)$ for all $k \in N$ . In this way, we guarantee the iterative command eventually terminates.

Understanding Loops

Consider loop $DO$ . Suppose a predicate $P$ satisfies

$P \land B_{i} ⟹ w p (S_{i}, P)$ for all $1 \leq i \leq n$ .

Suppose further that an integer function $t$ satisfies the following, where $t 1$ is a fresh identifier:

$P \land BB ⟹ (t > 0)$ ,
$P \land B_{i} ⟹ w p (^{″} t 1 : = t; S_{i}^{″}, t < t 1)$ , for $1 \leq i \leq n$ .

Then $P ⟹ w p (DO, P \land \neg BB)$ .