Modular Specification of Encapsulated Object-Oriented Components

In: Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, Willem-Paul de Roevered., Formal Methods for Components and Objects, Fourth International Symposium, FMCO 2005. LNCS, volume 4111, p. 313--341, 2006

Authors

• Arnd Poetzsch-Heffter
• Jan Schäfer

Abstract

A well-defined boundary of components allows to encapsulate internal state and to distinguish between internal calls that remain inside the component and external calls that have target objects outside the component. From a static point of view, such boundaries define the programmer's interface to the component. In particular, they define the methods that can be called on the component. From a dynamic point of view, the boundaries separate the component state and those parts of the program state outside the component.

In this tutorial paper, we investigate encapsulated components that are realized based on object-oriented concepts. We define a semantics that captures a flexible notion of hierarchical encapsulation with confined references. The semantics generalizes the encapsulation concepts of ownership types. It is used as a foundation for modular behavioral component specifications. In particular, it allows to provide a simple semantics for invariants and an alternative solution for the frame problem. We demonstrate this new specification methodology by typical programming patterns.

Full Text

• PDF: mod-spec-eoc.pdf
• PS.GZ: mod-spec-eoc.ps.gz

BibTeX

@InProceedings{Poetzsch-Heffter.Schaefer06modular, 
   author = {Arnd Poetzsch-Heffter and Jan Schäfer}
   title = {Modular Specification of Encapsulated Object-Oriented Components},
   booktitle = {Formal Methods for Components and Objects, Fourth International Symposium, FMCO 2005},
   series = {LNCS},
   publisher = {Springer},
   pages = {313--341},
   year = {2006},
}