A categorical treatment of pre- and post-conditions

DOI10.1016/0304-3975(87)90025-9MaRDI QIDQ1093363zbMATH OpenOpenAlexFDO

Authors Eric G. Wagner

Publication date 1987

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(87)90025-9

zbMATH Keywords

categories of interpretations Galois connection predicate transformers program specification

Mathematics Subject Classification ID

Special categories (18B99) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

This paper presents a treatment of pre- and post-conditions, and predicate transformers, in a category-theoretic setting. The meaning of a pair of pre- and post-conditions, or a predicate transformer, in a category is defined as a set of morphisms in that category. It is shown that this construction is natural in the sense that it forms part of a Galois connection. It is further proved that in the usual categories of interpretations (total functions, partial functions, and relations) pre- and post-conditions and predicate transformers have equal powers of specification and we characterize the specifiable sets of morphisms in these categories.

Recommendations

Cites work

Cited in

(7)

This page was built for publication: A categorical treatment of pre- and post-conditions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1093363)