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.