A categorical treatment of pre- and post-conditions
type: Item
instance of: scholarly article
title: A categorical treatment of pre- and post-conditions
zbMATH Open document ID: 0628.68017
DOI: 10.1016/0304-3975(87)90025-9
author: Eric G. Wagner
published in: Theoretical Computer Science
publication date: 1987-01-01T00:00:00Z
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.
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 18B99
zbMATH DE Number: 4022615
zbMATH Keywords: program specification
zbMATH Keywords: predicate transformers
zbMATH Keywords: Galois connection
zbMATH Keywords: categories of interpretations
MaRDI profile type: Publication
full work available at URL: 0304-3975(87)90025-9
OpenAlex ID: W2157120061
cites work: Q4174692
cites work: Programming as a Discipline of Mathematical Nature
cites work: Q3898534
cites work: Q3925859
cites work: Q5682456
cites work: An axiomatic basis for computer programming
cites work: Q3859249
cites work: Q5639839
cites work: Q5508993
cites work: Q3920613
cites work: Q3932278
cites work: Q3316563
cites work: Q3718134
cites work: Q4725716
description: scientific article; zbMATH DE number 4022615