Formalisms for Structural Operational Semantics

点击翻译按钮获取中文摘要

Operational semantics is a formal method of describing the meaning and behaviour of programming languages. Such methods are needed for automated program analysis, verification, translation or even construction. An operational specification describes how programs can perform actions and, at the same time, transform to other programs. Language designers have a wide choice of formalisms for writing operational descriptions of programs. In the so-called structural approach, the actions that a program may take are determined by the actions of its subprograms. In the reactive approach, program statements are thought to communicate with one another throughout the program structure to decide on the next action to take. The chosen formalism also depends on the kind of computational features used in the language, such as nondeterminism, probabilistic choice, real time, store, input/output, etc.Such a wide choice is welcome, but it can also be problematic. The large number of possible formalisms means that some of them are less thoroughly studied than other ones, and indeed it often happens that language designers create ad-hoc formalisms of their own, tailored to the needs of particular languages. They are then forced to check that their new formalism is meaningful and well-behaved, i.e., that it guarantees certain desirable properties of programs and facilitates reasoning about them.We aim at relieving language designers from some of this burden by developing a systematic, general approach to formalisms for operational semantics. We will study mathematical theories of both the structural and the reactive approach, aiming at a general theory of operational specifications. Such a theory will benefit programming language designers, facilitating the creation of new languages, the modification of existing ones, and the analysis of programs.