| |
Formal Models for Reasoning about Objects & Component Composition
Feb. 15, 2004
School of Computer Science, IPM
|
-
Frank de Boer, CWI (Centrum voor Wiskunde en Informatica)
Proof theory for Object Orientation
10:00-12:00
- Farhad Arbab , CWI (Centrum voor Wiskunde en Informatica)
A Foundation Model for Components and Their Composition.
14:00-16:00
- J.J.M.M. Rutten, CWI (Centrum voor Wiskunde en Informatica)
Concrete Coalgebra.
16:00-18:00
|
| Abstracts: |
Proof theory for Object Orientation
In this seminar I will discuss Hoare logics for object oriented programs. The Hoare logic is based on an assertion language which allows the description of properties of dynamic configurations of objects at an abstraction level that coincides with that of the programming language. Based on this assertion language I will introduce a weakest precondition calculus for reasoning about aliasing, object creation, and method calls. I will conclude with a discussion of compositionality and components. |
A Foundation Model for Components and Their Composition
We introduce the notion of an Abstract Behavior Type (ABT) as a proper foundation model for both components and their composition. An ABT defines an abstract behavior as a relation among a set of timed-data-streams, without specifying any detail about the operations that may be used to implement such behavior or the data types it may manipulate for its realization. The (generally) infinite streams that are the elements of behavior in the ABT model naturally lend themselves to the coalgebraic techniques and the coinduction reasoning principle. The ABT model supports much looser coupling than is possible with Object-Oriented models and is inherently amenable to exogenous coordination. We propose that both of these are highly desirable, if not essential, properties for components and their composition. |
In our view, a component based system consists of component instances and their connectors (i.e., the "glue code"), both of which are uniformly modeled as ABTs. As a concrete instance of the application of the ABT model, we present Reo: a channel-based exogenous coordination model wherein complex coordinators, called "connectors" are compositionally built out of simpler ones. The simplest connectors in Reo are a set of channels with well-defined behavior supplied by users. We demonstrate the surprisingly expressive power of connector composition in Reo through a number of examples. Because all Reo connectors are ABTs, we show how the semantics of channel composition in Reo can be defined in terms of a calculus of ABT composition.
|
Concrete Coalgebra
Coalgebras are the formal dual of algebras and have over the last decade or so become popular in both mathematics and computer science as unified models of various state-based dynamical systems, including: automata, transition systems, (infinite) data types, object- and component-based systems, Kripke models, discrete event systems, and many many more. In these lectures, we shall briefly review the basic notions of the discipline of coalgebra, which are bisimulation, finality, and coinduction. Next we shall mention, more concretely, a few particularly interesting and useful (final) coalgebras, notably streams, formal languages, and formal power series. Finally, we shall sketch a recent application of a coinductive calculus of bitstreams to sequential digital circuits, and show how this relates to the semantics of Reo, a framework for the compositional construction of component connectors, recently developed by Farhad Arbab.
|
Information |
| Place: | Lecture Hall, Niavaran Bldg., Niavaran Square, Tehran, Iran |
| Tel: | +98 21 2835060 |
| |
|
