Predicate Transformer Semantics (Cambridge Tracts in Theoretical Computer Science)
Predicate Transformer Semantics (Cambridge Tracts in Theoretical Computer Science)
Cambridge University Press | 1992-08-28 | ISBN: 0521420369 | 233 pages | DJVU | 2 MB
This book presents a rigorous foundation for defining Boolean categories, in which the relationship between specification and behavior is 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 a single program construct (the first-order theory of categories); others are 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.