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 $wp(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\Rightarrow wp(S,R)$.

Law of the Excluded Miracle

Given any command $S$, $wp(S,F)=F$

Distributivity of Conjunction

Given command $S$ and predicates $Q$ and $R$, $wp(S,Q\wedge R)=wp(S,Q)\wedge wp(S,R)$

Law of Monotonicity

Given command $S$ and predicates $Q$ and $R$, if $Q\Rightarrow R$, then $wp(S,Q)\Rightarrow wp(S,R)$.

Distributivity of Disjunction

Given command $S$ and predicates $Q$ and $R$, $wp(S,Q)\vee wp(S,R)\Rightarrow wp(S,Q\vee R)$

Commands

Skip

For any predicate $R$, $wp(skip,R)=R$.

Abort

For any predicate $R$, $wp(abort,R)=F$.

Sequential Composition

Sequential composition is one way of composing larger program segments from smaller segments. Let $S1$ and $S2$ be two commands. Then $S1;S2$ is defined as $wp{(}^{\prime \prime }S1;S{2}^{\prime \prime },R)=wp(S1,wp(S2,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 $wp{(}^{\prime \prime }x:=e^{\prime \prime },R)=domain(e)\text{ cand }{R}_e^x$ where $domain(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,\cdots ,x_n\circ s_n:=e_1,\cdots ,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 wp(''\bar{x} \coloneqq \bar{e}'', R) = domain(\bar{e}) \textbf{ cand } R_{\bar{e}}^\bar{x}

Alternative

The general form of the alternative command is: \begin{align*} \textbf{if } & B_1 \rightarrow S_1 \\ \textbf{ | } & B_2 \rightarrow S_2 \\ & \quad\cdots \\ \textbf{ | } & B_n \rightarrow S_n \\ \textbf{fi } & \end{align*}

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 $\text{IF}$ and define $\text{IF}$ in terms of $wp$ as: \begin{align*} wp(\text{IF}, R) = \;& (\forall i, 1 \leq i \leq n \Rightarrow domain(B_i)) \;\land \\ & (\exists i, 1 \leq i \leq n \land B_i) \;\land \\ & (\forall i, 1 \leq i \leq n \Rightarrow (B_i \Rightarrow wp(S_i, R))) \end{align*}

Bibliography

• Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.