Errata

On page 234, definition 10.3.4, of input and output identity, should have $\theta\overline{\mathord{?S}}$ for $\overline{\theta\mathord{?S}}$, and $\theta\overline{\mathord{!S}}$ for $\overline{\theta\mathord{!S}}$.

On page 244, the proof of Theorem 10.5.2 (Simple output refinement) adds an output to $AOp$ rather than to $Op$.

In Definition 10.5.2 (Upward IO Refinement), page 247, several things have gone wrong, all obvious except for the first:

• $IT$ should be injective;
• $OT_i$ should be total on concrete and abstract outputs rather than inputs;
• the antecedent of the correctness condition should be $COp_i \wedge T' \wedge !!OT_i$, i.e. $T$ should be replaced by $T'$;
• the outer universal quantification is also over $AState'$.