Are interface theories equivalent to contract theories?

Contract-based design is emerging as a unifying compositional paradigm for the specification, design and verification of large-scale complex systems. Different contract frameworks are currently available, but we lack a clear understanding of the relations between them. In this paper, we investigate the relation between interface theories (specifically, relational interfaces) and assume-guarantee (A/G) contracts. We introduce a natural transformation of interfaces to A/G contracts represented by linear temporal logic. Then, we analyze differences and correspondences between key operators and relations in the two theories (i.e. composition, refinement and conjunction), by studying their preservation properties under the proposed transformation. We show that the transformation preserves refinement, but does not generally preserve serial composition and conjunction. Then, we present an assumption-projection operator to make it possible to preserve serial composition and compatibility checking. Finally, we provide illustrative examples that shed light on the effectiveness of both frameworks for requirement formalization, early detection of integration errors, and use of abstraction-refinement.