  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.
