This paper abridges lecture notes from WOFACS 96. It provides semantic models for a variety of programming and development formalisms, showing how different models for the same formalism are related by Galois connections. ...

The refinement calculus, based on weakest preconditions, elaborates imperative program developments as a series of steps linked by a mathematical refinement relation. Specifications and executable code are regarded equally ...