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.
翻译:我们提出假设-保证(AG)契约的代数理论。我们定义了契约,提供了新的以及已知的运算,并展示了这些运算之间的关联。契约具有函子性质:任何布尔代数都关联了一个契约代数。我们研究了契约代数中的幺半群与半环结构,以及这些结构之间的映射。我们还讨论了布尔代数对其契约代数的作用。