An Algebraic Semantics for Contract-based Software Components

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.