The book distinguishes itself from all other works on program semantics in that the approach is nonoperational: 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 methodologicaily interested mathematicians. It is not designed as a textbook, although successful courses have been given based on this material.