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

spanmapmonotonic predicate transformerorder-enriched categorypullover

Mathematics Subject Classification ID

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

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

(17)

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

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)