Hypercontracts

Contracts (or interface) theories have been proposed to formally support distributed and decentralized system design while ensuring safe system integration. Over the last decades, a number of formalisms were proposed, sometimes very different in their form and algebra. This motivated the quest for a unification by some authors, e.g., specifications through contracts by Bauer et al. and the contract metatheory by Benveniste et al. to cite a few. These generic models establish precise links between the different contract frameworks. In this paper we propose hypercontracts, a generic model with a richer structure for its underlying model of components, subsuming simulation preorders. While this new model remains generic, it provides a much more elegant and richer algebra for its key notions of refinement, parallel composition, and quotient, and it allows considering new operations. On top of these foundations, we propose conic hypercontracts, which are still generic but come with a finite description. We show how to specialize conic hypercontracts to Assume-Guarantee contracts as well as to Interface Automata, two known contract frameworks very different in style. We illustrate conic hypercontracts on specifications involving security and the robustness of machine-learning components.