Towards a Theory of Architectural Contracts: Schemes and Patterns of Assumption/Promise Based System Specification

摘要

This paper presents basic concepts and paradigms for the specification and reasoning about systems, their interfaces and architectures as well as their properties in terms of contracts based on the idea of assumptions and promises. The key idea is that an assumption represents a specification of properties of the environment in which a system can be used, and that the promise describes the specification of properties of the system guaranteed under the assumption. Based on this idea explicit system specifications are derived forming implicative interface assertions. On this basis, more specific aspects of the specification and reasoning about properties of systems and their architectures in terms of assumptions and promises are analysed. What we study, in particular, is the fact that system assertions show some specific structure, for instance, in terms of liveness and safety properties as well as causality and realizability. This structure influences the meaning of assume/promise-specifications and imposes healthiness conditions for them.