On Specification and Correctness of OOD Frameworks in
Computational Logic

Kung-Kiu Lau  
Department of Computer Science 
University of Manchester 
Manchester M13 9PL, UK 
kung-kiu@cs.man.ac.uk 

Mario Ornaghi
Dipartimento di Scienze dell'Informazione
Universita' degli studi di Milano
Via Comelico 39/41, 20135 Milano, Italy
ornaghi@dsi.unimi.it

Abstract:
In current component-based software development (CBD), it is widely 
recognised that the distribution of tasks between objects and the
contracts between them are key to effective design. In composing
designs from reusable parts, increasingly the parts are
Object-oriented Design (OOD) frameworks, namely descriptions of the
interactive relationships between objects which participate in the
interactions. Designs are then built by composing these frameworks,
and any object in the final design will play (various) roles from
several frameworks. In this paper, we discuss our preliminary efforts
to define a formal semantics in computational logic for the specification
and correctness of OOD frameworks, and briefly illustrate it with
frameworks in the CBD methodology Catalysis. The novelty of our approach
is a priori correctness for OOD frameworks (and components in general)
and their composition, in contrast to current development methods
which are mainly in  the style of posit-and-prove, whereby proof
of correctness is done  by a posteriori verification. For
component-based software development, we argue that a priori
correctness is a better approach than a posteriori correctness.