Rafae Bhatti, Elisa Bertino, et al.
Communications of the ACM
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 specifications and we characterize the specifiable sets of morphisms in these categories. © 1987.
Rafae Bhatti, Elisa Bertino, et al.
Communications of the ACM
Sai Zeng, Angran Xiao, et al.
CAD Computer Aided Design
Frank R. Libsch, S.C. Lien
IBM J. Res. Dev
Victor Valls, Panagiotis Promponas, et al.
IEEE Communications Magazine