The original paper on hush is  [HUSH]. A veritable catalogue of object-oriented applications can be found in  [Harmon93]. A classical paper on class design is  [JF88]. For the Law of Demeter, consult  [LH89]. The notion of abstract systems was introduced in  [Henderson93], which also gives a good account of a formal approach to object-oriented design. For an introduction to formal methods and Z, consult  [Diller94]. For object-oriented extensions of Z, see  [Stepney].