,
Formal Derivation of Object-Oriented Designs
University of Queensland, (2007)
Аннотация
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 rigorous evolution of object-oriented specifications to derive designs in the Object-Z specification language. The proposed method carefully intertwines refinement with refactoring to formulate a theory that is both minimal and complete, in that any design may be derived from any specification if it is a valid refinement of the specification. The minimality of the rules stems from the fact that they each address orthogonal but fundamental aspects of object orientation. The Object-Z specification language was chosen as a vehicle for the approach, as it encompasses the complexities found in many objectoriented designs, particularly with respect to structural features and reference aliasing. Additionally, a novel method for undertaking compositional class refinement is described that facilitates the scalability of the overall approach by significantly reducing the burden of proof required for justifying refinement steps. The rules, methodology, and compositional refinement theory do not impose restrictions on the constructs used in specifications, nor do they restrict the syntax and semantics of the specification language. As such, the results of this thesis are applicable to any existing Object-Z specification that adheres to the modern language definition.
