Formal methods provide rigorous approaches and proof mechanisms for the development and verification of software systems. Much of the work in this field has focussed on refinement, which models the relationship between abstract specifications and more concrete specifications. For example, there are refinement theories that model the relationship between state machines specified at different levels of abstraction. However, the application of these theories to the object-oriented paradigm poses a significant challenge. Object orientation is useful primarily because of the modularity and reuse constructs it affords, and has become prevalent in industry for the implementation of large systems. Although object-oriented specification languages exist, two key issues are at the core of applying a refinement theory to these systems. The aforementioned modularity and reuse constructs (classes and objects) provide for a plurality of independent but interacting state machines, and refinement theory is hindered by the complex mapping between these local states and a unified global state. This is because refinement is not necessarily compositional in such an environment. Additionally, the specification of domain requirements in an object-oriented specification may not necessarily resemble—in a structural sense—the design of the desired implementation. Here, structure is interpreted as the relationships between or within classes and objects. This includes inheritance, instantiation, polymorphism, and type parameterisation (often referred to as templates or generics). As a result, there is a distinct gap between object-oriented specifications and object-oriented designs. It is the purpose of this thesis to address this gap, which is motivated by the existence of systems that are sufficiently large to warrant the object-oriented programming paradigm, but additionally require development under strict verification conditions. A novel set of rules and an accompanying methodology are presented that provide for the systematic and ...