PhD ThesisA computer program is a text in a de ned programming language; each such program can be thought of as de ning state transitions | that is, the execution of a program in an initial state will result in a (or possibly one of a set of) nal state(s). A program speci cation de nes properties that relate initial and nal states. For example, a speci cation might state that some property will hold in the nal state after the program has been executed, as long as it was executed in an initial state where some other property held. De ning the semantics of a programming language xes the behaviour of the language and gives meaning to programs that are written in the language. One straightforward way of giving the semantics of a programmi...