Developing Provably Correct Programs From
Object-Oriented Components

Peter Müller

Fachbereich Informatik, Fernuniversität
Feithstr. 140, 58084 Hagen, Germany
Tel: (++49 2331) 987-4870
Email: Peter.Mueller@fernuni-hagen.de

Arnd Poetzsch-Heffter

Fachbereich Informatik, Fernuniversität
Feithstr. 140, 58084 Hagen, Germany
Tel: (++49 2331) 987-304
Email: Arnd.Poetzsch-Heffter@fernuni-hagen.de

Abstract:

In object-oriented programming, component-based software construction is supported in four ways: by composition and specialization of classes, code inheritance, and genericity. Formal methods should allow to prove the correctness of a program component based on the specifications of its subcomponents without revisiting the implementations of these subcomponents. Essentially, two problems can occur: 1. Adding a new subtype S may violate the specification of its supertype T; thus components using T may be invalidated. 2. In certain cases, class invariants can be violated by adding new classes to existing components. This positional paper sketches the formal background needed to precisely formulate and investigate the above problems. It claims that behavioral subtyping is a solution to the first problem. As a possible solution to the second problem, it proposes techniques to make interface specifications more expressive, to restrict the form of invariants by semantical constraints (similar to behavioral subtyping), and to refine existing module concepts. It briefly discusses the relation of these techniques to code inheritance and genericity, and relates the problems to other work in the field.

Keywords: Components, formal specification, formal verification, object-oriented programs, behavioral subtyping, semantic modules

Workshop Goals: Discussing different approaches to the topic; learning from the experiences of practitioners; meeting people with similar focus; discussing possible cooperations.