2 Position

The objective of this positional paper is to draw a picture of the techniques needed to prove the correctness of a program-component based on the specifications of its subcomponents without revisiting the implementations of these subcomponents. We claim that the development of such techniques plays a key role in laying the foundation of component-based software and system construction.

We draw the picture for object-oriented programs that may exploit side-effects and destructive updates. We focus on object-oriented programs for three reasons: (1) Object-oriented languages provide support for component-based program development (see below). (2) The role of object-oriented languages in industrial software development becomes more and more important. (3) Encapsulation and explicit interfaces ease the specification and verification of programs. We do not exclude side-effects, because they are at least important for the specification and verification of low level program components and occur in most of the existing class libraries.

Object-oriented programming languages provide means to support component-based program construction: Specialization through subtyping/subclassing, code inheritance, and encapsulation mechanisms to guarantee integrity constraints on data representations. In today's software construction, this support is unfortunately limited to syntactic checks. Programmers are able to invalidate supertype specifications by adding subtypes or invariants of existing classes by adding new classes. As an example for the first problem consider a subtype LS of a list type where method insert of LS does nothing. Such misbehavior can in general not be detected by syntactic checking only. As an example for the second problem consider objects of a class C referencing objects of a class D. Assume that the invariant for C states that there is never a chain of references from C objects to C objects. By adding a new subtype of D that has a C attribute this invariant can be invalidated.

We claim that the use of semantic-based specification and verification techniques can overcome the above problems and lead to a systematic construction of correct program components from correct subcomponents. In addition to this, a precise semantical understanding will help to improve programming language constructs towards a better language support for component-based software construction.

Overview The rest of this section elaborates on the relation between component-based software construction and object-oriented programming. After that, we sketch the formal background needed to make later explanations sufficiently detailed. In section 3, we describe the problems involved with the relevant language features and sketch ideas for their solution. An overview of related work is given in section 4. Finally, we summarize expected benefits of our approach.

 

• 2.1 Component-Based Software
• 2.2 Formal Framework
  • Specification and Verification Technique
  • Meaning of Specifications