Read more
This book gives a self-contained foundation of predicate transformer semantics; it does so by making extensive use of the predicate calculus. The semantics of the repetitive construct is defined in terms of weakest and strongest solutions ; in terms of the weakest precondition and the weakest liberal precondition. The notion of determinacy is defined; it is shown how to cope with unbounded nondeterminacy without using transfinite induction. The book distinguishes itself from all other works on program semantics in that the approach is non operational: the definition is not in terms of a computational model. It distinguishes itself from many mathematical texts in that its proofs - which are short and elegant - follow a strict calculational format. It is a monograph for computing scientists with a mathematical inclination and for methodologically interested mathematicians. It is not designed as a textbook, though successful courses have been given based on this material.
List of contents
Contents: On Structures.- On Substitution and Replacement.- On Functions and Equality.- On our Proof Format.- The Calculus of Boolean Structures.- Some Properties of Predicate Transformers.- Semantics of Straight-Line Programs.- Equations in Predicates and Their Extreme Solutions.- Semantics of Repetitions.- Operational Considerations.- Converse Predicate Transformers.- The Strongest Postcondition.
