Some Algebraic Aspects of Assume-Guarantee Reasoning

TL;DR

This paper develops an algebraic framework for assume-guarantee contracts, exploring their operations, structures, and relationships within Boolean algebra contexts, providing a formal foundation for compositional reasoning.

Contribution

It introduces a formal algebraic structure for assume-guarantee contracts, including new operations and their relations, and studies their algebraic properties and functorial aspects.

Findings

Contracts form a functorial algebra over Boolean algebras

Identification of monoid and semiring structures in contract algebra

Analysis of Boolean algebra actions on contract algebra

Abstract

We present the algebra of assume-guarantee (AG) contracts. We define contracts, provide new as well as known operations, and show how these operations are related. Contracts are functorial: any Boolean algebra has an associated contract algebra. We study monoid and semiring structures in contract algebra -- and the mappings between such structures. We discuss the actions of a Boolean algebra on its contract algebra.