
Modular Structural Operational Semantics
Author(s) -
Peter D. Mosses
Publication year - 2015
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v12i7.21873
Subject(s) - modularity (biology) , modular design , computer science , semantics (computer science) , operational semantics , construct (python library) , programming language , equivalence (formal languages) , language construct , theoretical computer science , mathematics , genetics , discrete mathematics , biology
Modular SOS (MSOS) is a variant of conventional Structural Operational Semantics (SOS). Using MSOS, the transition rules for each construct of a programming language can be given incrementally, once and for all, and do not need reformulation when further constructs are added to the language. MSOS thus provides an exceptionally high degree of modularity in language descriptions, removing a shortcoming of the original SOS framework. After sketching the background and reviewing the main features of SOS, the paper explains the crucial differences between SOS and MSOS, and illustrates how MSOS descriptions are written. It also discusses standard notions of semantic equivalence based on MSOS. An appendix shows how the illustrative MSOS rules given in the paper would be formulated in conventional SOS.