Networking Research Laboratory
Department of Computer Sciences
The University of Texas at Austin
Director: Simon S.
Lam (more
publications)
A Theory of Interfaces and Modules I--Composition Theorem
Simon S. Lam and A. Udaya Shankar*
Abstract
We model a system as a directed acyclic graph
where nodes represent modules and arcs represent interfaces.
At the heart of our theory is a definition of
what it means for a module to satisfy a set of interfaces, as a service
provider for some and as a service consumer for others.
Our definition of interface satisfaction is designed to be
separable, i.e.,
interfaces encode adequate information such that
each module in a system can be designed and verified separately, and
composable, i.e.,
we have proved a composition theorem for the system model in general.
Index Terms:
Specification, verification, interfaces, modules, composition, decomposition,
composition theorem, separable design.
* A. Udaya Shankar is on the faculty of the Department of Computer Science,
University of Maryland, College Park
Authors' Note:
In this paper, we are concerned only with semantics. Upon this semantic foundation,
different languages for specifying interfaces and modules, as well as proof methods,
may be developed.