Proof One

Proof.

$$\langle \alpha[E/x] \rangle \; x := E \; \langle \alpha \rangle$$ (C.1)

Say state variables are $x_1,x_2,\dots,x_n,\;\; x_i \in X_i$ (without loss of generality). Now suppose assignment is $x_1 := E(x_1,x_2,\dots,x_n)$ (wlog). Let:

$$\beta(x_1,\dots,x_n) = \alpha[E(x_1,\dots,x_n),x_2,\dots,x_n]$$

$$= \alpha[E/x_1]$$

another predicate.

Suppose an input state vector $(a_1,a_2,\dots,a_n)$ satisfies $\beta$, so $\alpha(E(a_1,a_2,\dots,a_n),a_2,\dots,a_n)$ satisfies $\beta$, so $\alpha(E(a_1,a_2,\dots,a_n),a_2,\dots,a_n)$ is True . Now set $b_1 = E(a_1,a_2,\dots,a_n)$, so output vector is $(E(a_1,a_2,\dots,a_n),a_2,\dots,a_n)$. Then $\alpha(b_1,a_2,\dots,a_n) = \beta(a_1,a_2,\dots,a_n)$ is True . So this shows equation is correct.

Is $\beta = \alpha[E/x_1]$ as general as possible? Need to show any input to the assignment that satisfies the postcondition must also satisfiy the precondition. Put another way, we need to show that if the precondition $\beta$ is not satisfied, nor can the postcondition be.

So say $\beta(a_1,a-2,\dots,a_n) = \alpha(E(a_1,a_2,\dots,a_n),a_2,\dots,a_n)$ is False . Then letting $b_1 = E(a_1,a_2,\dots,a_n)$, the output of the assignment given input $(a_1,a_2,\dots,a_n)$ is $(b_1,a_2,\dots,a_n)$, and of course $\alpha(b_1,a_2,\dots,a_n) = \beta(a_1,a_2,\dots,a_n)$, which is False . $\qedsymbol$