Networking Research Laboratory
Department of Computer Sciences
The University of Texas at Austin
Director: Simon S.
A Theory of Interfaces and Modules I--Composition Theorem
Simon S. Lam and A. Udaya Shankar*
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
interfaces encode adequate information such that
each module in a system can be designed and verified separately, and
we have proved a composition theorem for the system model in general.
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
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.