An Oxford sequel to EWD1047

An Oxford sequel to EWD1047

In EWD1047 I mentioned

(30) $\left\lbrack {{P}{j}\text{true}v\text{true};Q}\right\rbrack \Rightarrow \left\lbrack {{P}{j}\text{true}}\right\rbrack \vee \left\lbrack {\text{true};Q}\right\rbrack$ (31) $\left\lbrack {P,\text{true}}\right\rbrack \vee \left\lbrack {\text{true},\neg P}\right\rbrack$ (32) $\left\lbrack {\text{true};\neg {X}_{i}\text{true}}\right\rbrack \sim \left\lbrack X\right\rbrack$

and showed how (31) follows from (30) and how (32) follows from (31), and remarked that I did not succeed in proving (30) from (31).

On December 18, 1990, He Jifeng sent me a proof of (30) from (31), which (with a minor correction in a hint) is included here on page EWD1089-1. His references are to the formulae as numbered in EWD1047.

On the 20th December, 1990, Stephen Brien, also from Oxford's Programming Research Group, sent me a derivation of (30) from (32), "thus showing that, given the other axioms of the relational calculus, (30), (31) and (32) are equivalent". His derivation (with a minor correction in a hint) is here included on page EWD 1089-2; formula (32) is referred to as "the cone rule".

It is interesting to note that in He Jifeng's proof all steps but 1 are equivalences; (31) is introduced in the same way as (32) in Stephen Brien's proof, viz. as conjunct.

A Proof of (30) from (31)

(30) $[P; \text{true} \vee \text{true}; Q] \Rightarrow [P; \text{true}] \vee [\text{true}; Q]$

Proof: Let

$$ X = \neg (\text {t r u e}; Q) $$

$$ Y = * (P; \text {t r u e}) $$

From (20) and (28) it follows that both $X$ and $Y$ are postconditions. Then one has

$$ \begin{array}{l} [ P; \text {t r u e} \vee \text {t r u e}; Q ] \ = {p r e d i c a t e c a l c u l u s a n d d e f o f X } \ [ X \Rightarrow P; \text {t r u e} ] \ = {X i s a p o s t c o n d i t i o n } \ [ \text {t r u e}; X \Rightarrow P; \text {t r u e} ] \ = {(1 5) a n d d e f o f Y } \ [ \text {t r u e} \Rightarrow * (X; Y) ] \ = \quad {(0) a n d (4) } \ [ (X; Y) \Rightarrow \text {f a l s e} ] \ = {p r e d i c a t e c a l c u l u s } \ [ \neg (X; Y) ] \ = {Y i s a p o s t c o n d i t i o n } \ [ \neg (X; \text {t r u e}; Y)) ] \ = \left{\left(3 1\right) a n d P := X \right} \ [ \neg (X; \text {t r u e}; Y) ] \wedge ([ X; \text {t r u e} ] \vee [ \text {t r u e}; \neg X ]) \ \Rightarrow \quad {p r e d i c a t e c a l c u l u s } \ \lnot (\text {t r u e}; Y) ] \vee [ \text {t r u e}; \neg X ] \ = {X a n d Y a r e p r e c o n d i t i o n s a n d (2 8) } \ \lnot Y ] \vee [ \lnot X ] \ = {(2 0) a n d d e f o f X a n d Y } \ \sim (P; \text {t r u e}) ] \vee [ \text {t r u e}; Q ] \ = \left{\left(2 0\right) a n d \left[ \text {t r u e} \equiv \sim \text {t r u e} \right] \right} \ P; \text {t r u e} ] \vee [ \text {t r u e}; Q ] \ \end{array} $$

￥

(30) $[P; true \vee true; Q] \Rightarrow [P; true] \vee [true; Q]$

Proof (using the cone rule):

$[P; \text{true} \vee \text{true}; Q]$ ${PredCalc}$ $[\neg (P; \text{true}) \Rightarrow \text{true}; Q]$ $= {\neg (P; true) \text{ is a precondition}}$ $\neg (P; \text{true}); \text{true} \Rightarrow \text{true}; Q]$ $\Rightarrow$ {Monotonicity of ;} [true; $\neg (P$ ; true); true $\Rightarrow$ true; true; $Q]$ $= {RelCalc}$ [true; $\neg (P$ ; true); true $\Rightarrow$ true; $Q]$ $= {Cone\text{Rule and} (P;true):=X}$ with $X:= (P, true)$ $\left([P; true] \vee [true; \neg (P; true); true]\right) \wedge [true; \neg (P; true); true \Rightarrow true; Q]$ $\Rightarrow$ ${PredCalc}$ $[P; \text{true}]\vee [\text{true}; \neg (P; \text{true}); \text{true} \wedge (\text{true}; \neg (P; \text{true}); \text{true} \Rightarrow \text{true}; Q)]$ $\Rightarrow$ ${PredCalc}$ [P; true] $\vee$ [true; $Q$ ]

I than both gentlemen for their contributions.

Austin, 16 January 1991

prof. dr. Edsger W. Dgksta

Department of Computer Sciences

The University of Texas at Austin

Aushin, TX 78712 - 1188

USA