Formalisms for Structural Operational Semantics

操作语义学是描述程序设计语言的意义和行为的一种形式化方法。自动化程序分析、验证、翻译甚至构造都需要这样的方法。操作规范描述了程序如何执行操作，同时转换为其他程序。语言设计者在编写程序的操作描述时有很多形式选择。在所谓的结构化方法中，一个程序可能采取的动作是由它的子程序的动作决定的。在反应式方法中，程序语句被认为在整个程序结构中相互通信，以决定下一步要采取的行动。所选择的形式主义还取决于语言中使用的计算特征的种类，例如非确定性、概率选择、真实的时间、存储、输入/输出等。如此广泛的选择是受欢迎的，但也可能是有问题的。大量可能的形式主义意味着它们中的一些比其他的研究得更少，实际上，语言设计者经常创建自己的ad-hoc形式主义，以适应特定语言的需求。然后，他们被迫检查他们的新形式主义是有意义的和行为良好的，即，它保证了程序的某些理想属性，并促进了对它们的推理。我们的目标是通过开发一个系统的，通用的方法来形式化操作语义，以减轻语言设计者的一些负担。我们将研究数学理论的结构和反应的方法，旨在操作规范的一般理论。这样的理论将有利于编程语言设计者，促进新语言的创建，现有语言的修改和程序的分析。

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.