形式语义描述方法研究进展与评价  

Research and Evaluation on Formal Semantic Description Techniques

作　　者：张迎周[1] 张卫丰[1] 钱俊彦[2] 

机构地区：[1]南京邮电大学计算机学院,江苏南京210003 [2]桂林电子工业学院计算机系,广西桂林541004

出　　处：《南京邮电大学学报（自然科学版）》2006年第6期86-94,共9页Journal of Nanjing University of Posts and Telecommunications：Natural Science Edition

基　　金：国家自然科学基金(60503020);江苏省高校自然科学基金(05KJD520151);广西自然科学基金(0542036)资助项目

摘　　要：程序设计语言形式语义描述技术在1990年代进入新一轮发展高潮,它对程序设计语言的设计和标准化,编译程序的设计和优化,程序推理,以及安全协议形式化描述、分析验证与设计等都有着重要的意义。但不同于成熟统一的形式化语法描述技术,语义的形式描述技术尚处于蓬勃发展和多种技术并存时期。首先回顾形式语义描述方法的研究发展史;然后通过实例介绍当前主要的语义形式描述方法;最后给出这些方法的评价标准和比较结果,并指出最有发展潜力的语义描述方法,以及将来的发展方向。The 1990s witnessed the new developments on formal description techniques of program semantics. These techniques are significant for design, reasoning and standardization of programming languages, and for design and optimization of compiler as well. They have been widely used in formal description, analysis, verification and design of security protocols. In sharp contrast to the popularity of formal syntax, formal semantic descriptions have seldom been exploited in practical applications concerning design and implementation of programming languages. In this paper, we firstly review the history of development for semantic description frameworks of programming languages. Then we illustrate and assess the features of main frameworks of current interest. Finally, we give the qualitative comparisons of these frameworks distinctly. We conclude that the abstract state machine （ASM） and modular monadic action semantics （MMAS） approaches are two good candidates for such a framework.

关 键 词：形式化语义描述 安全协议分析 博弈语义 单子语义 

分 类 号：TP311.1[自动化与计算机技术—计算机软件与理论]