Predicate Transformer Semantics

Ernest. G. Manes

doi:10.1017/CBO9780511569821

- Get access
  
  Buy a print copy
  
  Check if you have access via personal or institutional login
  
  Log in Register
Cited by 9
Cited by
- 9
Crossref Citations

This Book has been cited by the following publications. This list is generated based on data provided by Crossref.

Manes, Ernest G. 1992. Mathematical Foundations of Programming Semantics. Vol. 598, Issue. , p. 446.

CrossRef

Google Scholar

Manes, Ernest G. 1993. Fundamentals of Computation Theory. Vol. 710, Issue. , p. 363.

CrossRef

Google Scholar

Manes, E. G. 1993. Adas and the equational theory of if-then-else. Algebra Universalis, Vol. 30, Issue. 3, p. 373.

CrossRef

Google Scholar

Jay, C. Barry and Cockett, J. R. B. 1994. Programming Languages and Systems — ESOP '94. Vol. 788, Issue. , p. 302.

CrossRef

Google Scholar

Bloom, Stephen L. and Ésik, Zoltán 1994. Mathematical Foundations of Computer Science 1994. Vol. 841, Issue. , p. 52.

CrossRef

Google Scholar

Bloom, Stephen L. and Ésik, Zoltán 1994. Mathematical Foundations of Programming Semantics. Vol. 802, Issue. , p. 378.

CrossRef

Google Scholar

COCKETT, ROBIN and MANES, ERNIE 2009. Boolean and classical restriction categories. Mathematical Structures in Computer Science, Vol. 19, Issue. 2, p. 357.

CrossRef

Google Scholar

Hoefnagel, Michael 2020. M-coextensive objects and the strict refinement property. Journal of Pure and Applied Algebra, Vol. 224, Issue. 10, p. 106381.

CrossRef

Google Scholar

Huerta y Munive, Jonathan Julián and Struth, Georg 2022. Predicate Transformer Semantics for Hybrid Systems. Journal of Automated Reasoning, Vol. 66, Issue. 1, p. 93.

CrossRef

Google Scholar

Ernest. G. Manes, University of Massachusetts, Amherst

Publisher:: Cambridge University Press
Online publication date:: January 2010
Print publication year:: 1992
Online ISBN:: 9780511569821
DOI:: https://doi.org/10.1017/CBO9780511569821

Subjects:: Algorithmics, Complexity, Computer Algebra, Computational Geometry, Computer Science, Programming Languages and Applied Logic
Series:: Cambridge Tracts in Theoretical Computer Science (33)

51.99 (GBP)

Digital access for individuals
(PDF download and/or read online)
Add to cart

Added to cart

Digital access for individuals
(PDF download and/or read online)
View cart
Export citation
Buy a print copy

Information

Contents

Metrics

A central problem in the design of programming systems is to provide methods for verifying that computer code performs to specification. This book presents a rigorous foundation for defining Boolean categories, in which the relationship between specification and behaviour can be explored. Boolean categories provide a rich interface between program constructs and techniques familiar from algebra, for instance matrix- or ideal-theoretic methods. The book's distinction is that the approach relies on only a single program construct (the first-order theory of categories), the others being derived mathematically from four axioms. Development of these axioms (which are obeyed by an abundance of program paradigms) yields Boolean algebras of 'predicates', loop-free constructs, and a calculus of partial and total correctness which is shown to be the standard one of Hoare, Dijkstra, Pratt, and Kozen. The book is based in part on courses taught by the author, and will appeal to graduate students and researchers in theoretical computer science.

- Aa Reduce text
- Aa Enlarge text

View selected items
Save to my bookmarks
Export citations
Download PDF (zip)
Save to Kindle
Save to Dropbox
Save to Google Drive
Save content to
To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to .

To save content items to your Kindle, first ensure [email protected] is added to your Approved Personal Document E-mail List under your Personal Document Settings on the Manage Your Content and Devices page of your Amazon account. Then enter the ‘name’ part of your Kindle email address below. Find out more about saving to your Kindle.

Note you can select to save to either the @free.kindle.com or @kindle.com variations. ‘@free.kindle.com’ emails are free but can only be saved to your device when it is connected to wi-fi. ‘@kindle.com’ emails can be delivered even when you are not connected to wi-fi, but note that service fees apply.

Find out more about the Kindle Personal Document Service.

Please be advised that item(s) you selected are not available.
You are about to save
Your Kindle email address

Please provide your Kindle email.

@free.kindle.com @kindle.com (service fees apply)

By using this service, you agree that you will only keep content for personal use, and will not openly distribute them via Dropbox, Google Drive or other file sharing services

Metrics

Total number of HTML views: 0

Total number of PDF views: 0 *

Loading metrics...

Total views: 0 *

Loading metrics...

* Views captured on Cambridge Core between #date#. This data will be updated every 24 hours.

Usage data cannot currently be displayed.

Predicate Transformer Semantics

This Book has been cited by the following publications. This list is generated based on data provided by Crossref.

Book description

Refine List

Actions for selected content:

Contents

Frontmatter
pp i-vi

Contents
pp vii-viii

Preface
pp ix-x

Introduction
pp 1-22

Part I - Finite Coproducts
pp 23-23

1 - Fundamental Frameworks
pp 23-30

2 - Natural Choice Operators
pp 31-45

3 - Polymorphic Iterates
pp 46-70

Part II - Structure of a Boolean Category
pp 71-71

4 - The Axioms
pp 71-79

5 - The Boolean Algebra of Summands
pp 80-89

6 - Null and Total Morphisms
pp 90-97

7 - Preadditive Categories
pp 98-105

8 - Projections and Guards
pp 106-117

9 - Hoare Assertions and while-do
pp 118-130

10 - Predicate Transformers
pp 131-145

Part III - Metatheory
pp 146-146

11 - Representations by Relations
pp 146-160

12 - Deterministic Morphisms
pp 161-170

13 - Completion and Duality
pp 171-181

14 - Equations for 3-valued if-then-else
pp 182-187

Part IV - Distributive Categories
pp 188-190

15 - Atomic Morphisms
pp 190-198

16 - Boolean Monads
pp 199-215

Bibliography
pp 216-220

Index
pp 221-223

Metrics

Full text views

Book summary page views

Predicate Transformer Semantics

Book description

Refine List

Actions for selected content:

Save Search

Contents

Metrics

Full text views

Book summary page views