Towards a Meta-Theory of Operational Semantics

Introduction There are several ways to give a semantics of a programming language. Each kind of semantics gives a different insight into the meaning of a language, and is useful for different tasks. The axiomatic approach specifies a language by means of the properties it possesses. Such a specification need not necessarily be complete. Examples of such systems are Hoare Logic [Apt81] and Dijkstra's predicate transformers [DS90]. . Such a semantics is useful when one is still working out the details of the language, and also for highlighting important features to users. The denotational approach is to define a function from programs to their meanings. These meanings, or denotations, are mathematical values which represent the result of running the program. Such a semantics is useful for users and designers of languages. Schmidt [Sch88] contains an excellent introduction to denotational semantics. The operational approach is to define a kind of mathematical mac