The Relatedness and Comparative Utility of Various Approaches to Operational Semantics

We examine three approaches to operational semantics: transition semantics, natural semantics, and reduction semantics. First we compare the style and expressive power of the three forms of semantics by using them to construct semantics for various language features. Program abortion, interleaving, and block structure particularly distinguish the three. Natural semantics was very good at specifying "large granularity" features such as blocks, but is apparently unable to capture interleaving because of its "small granularity". On the other hand, transition semantics and reduction semantics easily express "small granularity" features but have difficulty with "large granularity" features. Reduction semantics provide especially concise specifications of non-sequential control constructs such as abortion and interleaving. We also analyze the utility of the different approaches for two application areas: implementation correctness and type soundness. For these two applications, natural semantics seems to allow simpler proofs, although we do not generalize this conclusion to other areas.