2.1 Component-Based Software

Our view of component-based software construction is as follows: We assume a set of basic components contained in a software library. Each basic component is a module which contains a set of classes. All classes contained in such libraries are assumed to be formally specified and verified. The interesting task of component-based software construction is to use these basic components to build more complex pieces of software. In particular, we want to study how correctness of such complex components can be derived from the specifications of the used basic components. In terms of modules, we want to prove the correctness of a new module based on the correctness of imported modules.

Object-oriented languages support three techniques to build complex components: (1) Composition, (2) inheritance, and (3) genericity. Composition means to put together different components to use the functionality of all of them. In most cases, existing components have to be customized before they can be combined with other components. This can be done by inheritance and genericity. By means of inheritance, new components can be gained from existing ones by inheriting their code and adding new functionality. E.g., a class for sorted lists can be developed by using code of a simple list class and adding a method sort. Genericity can be used to parameterize types. E.g., one can implement a generic class list which can be instantiated to lists of integers, booleans, or any other type. We will discuss the effects of these techniques on program correctness in section 3.