A theory of interfaces and modules I-composition theorem

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