An Algebraic Semantics for Contract-based Software Components
- Prelegent(ci)
- Artur Zawłocki
- Afiliacja
- Uniwersytet Warszawski, Instytut Informatyki
- Termin
- 20 października 2008 10:15
- Pokój
- p. 4790
- Seminarium
- Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji
Praca Michela Bidoit i Rolfa Hennickera (z AMAST 2008)
Abstrakt pracy:
We propose a semantic foundation for the contract-based design of
software components. Our approach focuses on the characteristic
principles of component-oriented development, like provided and
required interface specifications and strong encapsulation.
Semantically, we adopt classical concepts of mathematical logic using
models, in our framework given by labelled transition systems with
``states as algebras'', sentences, and a satisfaction relation which
characterizes those properties of a component which are observable by
the user in the ``strongly reachable'' states. We distinguish beteween
models of interfaces and models of component bodies. The latter are
equipped with semantic encapsulation constraints which guarantee, that
if the component body is a correct user of the required interface
operations, then it can safely rely on all properties of the required
interface specification. Our model-theoretic semantics of interfaces
and component bodies suggests two semantic views on a component, its
external and its internal semantics which must be properly related to
ensure the correctness of a component. We also study a refinement
relation between required and provided interface specifications of
different components used for component composition.