We consider Stone algebras with a distinguished element e satisfying the identity e → x = ¬ ¬ x for all elements x of the algebra. We provide an adjunction between the category of such algebras and that of Boolean algebras. This adjunction turns out to involve the concept of assume-guarantee contracts, which has numerous applications throughout engineering and computer science.
Keywords: Stone algebras, contracts, assume-guarantee reasoning
2020 MSC: 08A70, 08C05
Theory and Applications of Categories, Vol. 41, 2024, No. 57, pp 2041-2057.
Published 2024-12-09.
TAC Home