Enhanced operational semantics
Enhanced operational semantics
复制标题
增强的操作语义
DOI：
--
复制
发表时间：
1996
期刊：
影响因子：
--
通讯作者：
C. Priami
中科院分区：
文献类型：
--
作者：
P. Degano;C. Priami
机器的行为可以通过一种操作方法方便地给出，该方法描述了机器在计算时执行的状态之间的转换。这些状态和跃迁，可能由它们所代表的活动来标记，产生了一个跃迁系统。由于Plotkin和他的形式化方法，称为结构操作语义学[Plotkin 1981; Nielson and Nielson 1992]，操作语义学的逻辑方法利用了语言和抽象机器之间的二元性，因此人们通过归纳机器本身的句法结构来推导转换。我们提出了一个增强的结构化操作语义能够表达（几乎）在软件生产过程中所需的所有信息。事实上，我们的方法可以很容易地专门化，既可以覆盖与项目阶段相关的各个不同方面，又可以在实现方面越来越详细地细化规范。操作语义在数学上是简单的，接近直觉，从而为实现提供了指导。它允许使用归纳法来证明程序的性质。这种方法比其他方法更适合处理包含异构特性的编程语言。事实上，它已经成功地用于描述命令式、函数式、逻辑、面向对象、并发和分布式语言。语义应该支持系统生产过程中执行的许多不同活动：设计，实现，质量控制，管理，使用等。因此，许多利益相关者（设计者，实现者，用户）必须理解它。他们可以大致分为两大类。第一组对系统的行为方面特别感兴趣（即，不管他们做什么，不管他们做什么。另一组关注系统的定量方面（即，如何有效地执行）。这些考虑需要一个尽可能可用的语义学，以及一个相应简单的基础理论。操作语义是这样的，因为它描述了任何计算设备所具有的基本特征。因此，最终用户也可以通过他们在自己的机器上的经验来理解定义的含义。此外，它是足够的装饰过渡系统与相关的信息来详细描述复杂的系统。例如，可以增强操作语义来描述我们在这里更详细讨论的并发和分布式进程的各个方面，例如因果关系，局部性（所谓的真正并发），优先级，时间和概率。这些行为和量化方面有助于提高代码的质量和健壮性，以及系统的有效运行时管理。同一系统的不同视图导致了许多不同的语义，这些语义必须通过
The behavior of machines is conveniently given by an operational approach that describes the transitions between states that a machine performs while computing. The states and the transitions, possibly labeled by the activity they represent, give rise to a transition system. A logical approach to operational semantics due to Plotkin and to his formal method, called structural operational semantics [Plotkin 1981; Nielson and Nielson 1992], exploits the duality between languages and abstract machines, so one deduces transitions by inducing on the syntactic structure of the machine itself. We propose an enhancement to structural operational semantics capable of expressing (almost) all the information needed during software production. Indeed, our approach can be easily specialized, both to cover the various different aspects relevant to the project phase and to refine in more and more detail specifications towards implementations. Operational semantics is mathematically simple and is close to intuition, thus giving guidelines for implementation. It permits the use of induction for proving properties of programs. This approach is better suited than others to cope with programming languages that include heterogeneous features. In fact, it has been successfully used to describe imperative, functional, logic, object-oriented, concurrent, and distributed languages. Semantics should support many distinct activities performed during system production: design, implementation, quality control, management, use, and so on. Therefore many stakeholders (designers, implementors, users) must understand it. They can be roughly divided in two main groups. The first group is particularly interested in the behavioral aspects of systems (i.e., in what they do, regardless of how). The other group is concerned with the quantitative aspects of systems (i.e., how efficiently they perform). These considerations call for a semantics as usable as possible, with an accordingly simple underlying theory. Operational semantics is such because it describes the essential features that any computing device has. Thus, also, end users can grasp the meaning of a definition driven by their experience on their own machines. Moreover, it is sufficient to decorate transition systems with the relevant information to describe complex systems in detail. For example, one can enhance operational semantics to describe aspects of concurrent and distributed processes that we discuss here in more detail, such as causality, locality (so-called true concurrency), priorities, time, and probabilities. These behavioral and quantitative aspects help improve the quality and robustness of code and efficient runtime management of systems. Different views of the same system have led to many different semantics that must be related to one another via