Ruixiong Tian, Zhe Xiang, et al.
Qinghua Daxue Xuebao/Journal of Tsinghua University
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.
Ruixiong Tian, Zhe Xiang, et al.
Qinghua Daxue Xuebao/Journal of Tsinghua University
Rajiv Ramaswami, Kumar N. Sivarajan
IEEE/ACM Transactions on Networking
Khaled A.S. Abdel-Ghaffar
IEEE Trans. Inf. Theory
S.M. Sadjadi, S. Chen, et al.
TAPIA 2009