Application-oriented program semantics

Abstract

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 formalisms are: the language of guarded commands and its refinement calculus; communicating sequential processes; and probabilistic imperative code. The semantic models include: binary relations; predicate transformers; traces; failures; and distributions. In each case, denotations of code are characterised, in the more general specification space, by the healthiness conditions they satisfy. Models are evaulated for their elegance, expressive power and calculational facility. Expanded notes containing proofs, an extra chapter on data refinement and exercises for each chapter, are available from the au­thors.