next up previous contents
Next: Example Up: Concatenation (Composition) Rule Previous: Concatenation (Composition) Rule   Contents

Proof of Soundness

Assume the hypothesis (are partially correct tripples). Suppose input $ x$ satisfies $ \alpha$. Apply $ P$ to it, then $ Q$. Then after applying $ P$ to $ x$, any result satisfies $ \beta$. So wehn $ Q$ is applied to that, the result (if any) satisfies $ \gamma$ (by the correctness of $ \langle \beta \rangle \; Q \; \langle \gamma \rangle $). So by definition, $ \langle \alpha \rangle \; P;Q \; \langle \gamma \rangle $ is partially correct.


David Goodwin 2008-09-20