University of Texas at Austin Department of Computer Sciences
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*

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.