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.