An algebraic construction of predicate transformers

DOI10.1016/0167-6423(94)90006-XMaRDI QIDQ1330446zbMATH OpenOpenAlexFDO

Authors Paul H. B. Gardiner, C. E. Martin, Oege de Moor

Publication date 19 February 1995

Published in Science of Computer Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0167-6423(94)90006-x

zbMATH Keywords

mapmonotonic predicate transformerorder-enriched categorypulloverspan

Mathematics Subject Classification ID

Theories (e.g., algebraic theories), structure, and semantics (18C10) Enriched categories (over closed or monoidal categories) (18D20) Semantics in the theory of computing (68Q55) Abstract data types; algebraic specification (68Q65)

Review text

The paper deals with the assignments \[ C \mapsto \text{Map} C, \quad C \mapsto \text{Span} C \] for certain preorder-enriched categories [cf. \textit{A. Carboni}, \textit{S. Kasangian} and \textit{R. Street}, ``Bicategories of spans and relations, J. Pure Appl. Algebra 33, 259-267 (1984; Zbl 0577.18005)] and gives conditions for these operators to be inverse to each other. Several applications as indicated by the title are presented in detail.

Recommendations

• scientific article; zbMATH DE number 512951
• A recursion theorem for predicate transformers on inductive data types
• A categorical treatment of pre- and post-conditions
• Towards a calculus of predicate transformers
• scientific article; zbMATH DE number 3999260

Cited in

(18)

• A categorical treatment of pre- and post-conditions
• A predicate transformer for the progress property `to-always'
• Soundness of data refinement for a higher-order imperative language
• Calculating sharp adaptation rules.
• Generic transformations of predicate encodings: constructions and applications
• Power simulation and its relation to traces and failures refinement
• Data refinement, call by value and higher order programs
• Towards patterns for heaps and imperative lambdas
• A program construction and verification tool for separation logic
• scientific article; zbMATH DE number 512951 (Why is no real title available?)
• The algebra of multirelations
• Category theoretic models of data refinement
• Trace-relating compiler correctness and secure compilation
• Computer Science Logic
• A presheaf semantics for quantified temporal logics
• Predicate transformers and higher-order programs
• Formalizing Dijkstra's predicate transformer wp in weak second-order logic
• Counterpart-based quantified temporal logics

This page was built for publication: An algebraic construction of predicate transformers

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