For algebraic specifications a well-developed theory supporting formal developments is available [Wirs 90]. In particular, the fundamental implementation relation is transitive and monotonic and therefore satisfies the horizontal and vertical composition property. Using the equations of "module algebra" structured specifications can be transformed into various normal forms and structured proof calculi allow one to verify the correctness of implementations in a structured way [Wirs 91]. Context induction provides a new method for verifying behavioural implementations [Henn 90]. Most of these results can be extended to object oriented specifications [Breu 91].