Mathematical Structural Operational Semantics

数学结构运算语义

• 批准号: EP/D039045/1
• 负责人: Gordon Plotkin
• 金额: $ 15.89万
• 依托单位: University of Edinburgh
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2006
• 资助国家: 英国
• 起止时间: 2006 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FD039045%2F1
• 关键词: Mathematical; Structural; Operational; Semantics

Structural operational semantics (SOS) 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 SOS specification describes how programs can perform actions and, at the same time, transform to other programs. The actions that a program may take are determined by the actions of its subprograms. This semantical method is popular among researchers, and many simple languages have been specified this way, but a comprehensive theory is needed to help language designers write well-structured and well-behaved operational semantics.We aim at such a formal, mathematical theory of SOS. We plan to treat formats for operational specifications that guarantee some desirable properties of programs, provide logics for reasoning about programs, enable reasoning about translations between programming languages, and give means for the modular construction of operational semantics.Such a theory will benefit programming language designers, facilitating the creation of new languages, the modification of existing ones, and the analysis of programs.

结构操作语义学（Structural Operational Semantics，SOS）是一种描述程序设计语言的意义和行为的形式化方法。SOS规范描述了程序如何执行操作，同时如何转换为其他程序。一个程序可能采取的动作是由它的子程序的动作决定的。这种语义方法在研究人员中很流行，许多简单的语言都是这样描述的，但是需要一个全面的理论来帮助语言设计者编写结构良好、行为良好的操作语义。我们计划处理操作规范的格式，保证程序的一些理想的属性，提供逻辑推理程序，使推理程序语言之间的翻译，并给出方法的模块化结构的操作语义。这样的理论将有利于程序设计语言的设计者，促进新的语言的创建，现有的修改，和程序的分析。

项目成果

Structural operational semantics for stochastic systems

随机系统的结构操作语义

• 发表时间: 2008
• 作者: N/a Klin