Beomseok Nam, Henrique Andrade, et al.
ACM/IEEE SC 2006
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.
Beomseok Nam, Henrique Andrade, et al.
ACM/IEEE SC 2006
Alfonso P. Cardenas, Larry F. Bowman, et al.
ACM Annual Conference 1975
Sai Zeng, Angran Xiao, et al.
CAD Computer Aided Design
B.K. Boguraev, Mary S. Neff
HICSS 2000