The thesis is available at: http://www.ifi.uio.no/~ftp/publications/dr-scient-theses/
The main conclusions are found in this PostScript file. A paper for FMOODS`96 describes a version of the formal object-oriented language Omicron used in the thesis. A PostScript version is found here.
Abstract:
This thesis presents a formal model of object-oriented concepts as
found among experienced designers of maintainable and reusable
software components. The formal frameworks have been used to find
necessary and sufficient requirements on sets of objects and
similarity relations between such sets in order to assure that when
sets of objects are substituted in a system, then the rest of the
software in the system will observe no difference. Many of these
requirements correspond with common design practices while there are
some additional requirements. If or when these new requirements are
incorporated into existing practices then the result will, hopefully,
be more efficient system development and maintenance.
Existing applications and systems composed from software components can also be extended by substituting existing components with new ones. The term extensible systems is used for such systems. According to Pountain in Byte May 1994 it is "the software engineers nirvana" when functionality can be changed or added to an extensible systems at runtime by substituting components.
In this tradition, experienced designers' classify components by the components collaborative behaviour. This is done to enhance the ability to compose and reuse software. Similarity of components is based on the principle that two similar components can be substituted without the rest of the software in the system observing any difference. Additionally, to avoid new errors, a component must behave in a similar way even when other components in the system are substituted with components with similar behaviour. We say that when this additional requirement holds for similar components, then one component can safely substitute for the other.
At present the most succesfull extensible systems are built using object-oriented components. To support reasoning about such object-oriented components this thesis introduce an object-oriented calculus. The calculus, called Omicron, is based on a simple object-oriented language and gives a formal definition of the semantics of this language. The calculus directly models the concepts used by experienced designers of reusable object-oriented components: object identity, object creation, encapsulation, inheritance and message sending. The calculus is used ot reason about properties of components consisiting of typically more than one object.
The main result of the thesis is a formal definition of "safely substitutable components". The result include a list of requirements on component and similarity definitions which are necessary and sufficient to formally prove safe substitution. It is shown that many of these requirements correspond with component designers' recommendations on how to design reusable components while other requirements are previously unknown, but should be incorporated into design notations and practices. Using the new results will, hopefully, better support the design of reusable and maintainable components and give more efficient system development and maintenance.
The title "divide et impera" is motivated by the idea of splitting a large system into manageable components. One of the main results of this thesis is a description of how to create components so that systems work as planned when building and maintaining them by manipulating their manageable components.
The calculus is published in Omicron, An Object-Oriented Calculus, Paper for the 1st IFIP Workshop on Formal Methods for Open Object-based Distributed Systems (FMOODS), Paris, 2-6 March, 1996. Postscript version