Homepage>Publikationen>PublikationsDetail

Developing Provably Correct Programs From Object-Oriented Components

In: Leavens, Gary T. and Sitaraman, Muralied., Foundations of Component-Based Systems. Available. HTML version available from http://www.cs.iastate.edu/~leavens/FoCBS/FoCBS.html, 1997

Authors

Peter Müller
Arnd Poetzsch-Heffter

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.

Full Text

PDF: focbs97.pdf
PS.GZ: focbs97.ps.gz

BibTeX

@InProceedings{Mueller.Poetzsch-Heffter97developing, 
   author = {Peter Müller and Arnd Poetzsch-Heffter}
   title = {Developing Provably Correct Programs From Object-Oriented Components},
   booktitle = {Foundations of Component-Based Systems},
   note = {Available. HTML version available from http://www.cs.iastate.edu/~leavens/FoCBS/FoCBS.html},
   year = {1997},
}

Einloggen