page 7, To avoid the types of the output parameters clashing the operation Leave of class Multiplexer should be defined as follows.

        Leave = output.Leave /\ source.Leave_\ (item!)

page 65, The value of  phi([false]) should be [delta(n) | n> 10 /\ n'=n].

page 66, The values of chi([false]), chi(chi([false])), chiⁱ⁺¹([false]) and Op₁ should be 
[delta(n) | false]. 

page 99, To appropriately constrain variables which are changed by only the first operation of a sequential composition, the predicate of the second schema in the definition should include the following. 

        w₁'=w₁ /\ ... /\ w_p'=w_p   where delta(Op₁) \ delta(Op₂) = {w₁,...,w_p}.

page 137, The scope enrichment operator should bind less tightly than all other binary operators. The hiding operator should bind more tightly than all binary operators except sequential composition. 

page 143, The final reference should be the following.

        Stepney, S., Barden, R. and Cooper, D. (eds) (1992) Object Orientation in Z,   Springer-Verlag.