面向对象程序设计语言的形式语义研究

面向对象程序设计语言(以下简称面向对象语言)的基本思想起源于六十年代中期的Simula语言,在七十年代的Smalltalk语言及环境中得到发展,在八十年代的Eiffel、C++等语言中进一步得到巩固和完善。

程序设计语言的形式语义研究进展

程序设计语言形式语义描述方法的产生与发展,对程序设计语言的设计和标准化,编译程序的设计和优化,程序推理,以及协议形式化描述、分析验证与设计等都有着重要的意义。回顾形式语义描述方法的研究发展史,介绍当前主要的语义形式描述方法,并给出这些方法的评价标准和比较结果;指出最有发展潜力的语义描述方法以及将来的发展方向。

一个说明语言的设计和其子集编译器的开发

基于软件文档可执行的想法，设计了一个适用于指称语义描述的可执行规范说明语言——ＪＺＣ，并对其核心子集编译器进行了设计与开发。该语言设计采用了模式匹配、类型并置和构造函数等概念，使得抽象文法易于在程度中体现。模块概念的引入使得函数型语言书写的程序更加易懂和易于编写。作为对严格开发方法的一个尝试，ＪＺＣ核心子集编译器的开发采用了该种方法，其中一个“结果正确性定理”的证明是开发过程的重点工作。本文通过一个示例语言简介ＪＺＣ的语言特点。

一种面向对象的函数式语言

设计了一种对象式和函数式相结合的混合型语言ＯＯＦＬ（面向对象的函数式语言），详细给出了它的语法及语义定义，提出了相应的实现方案，并在微机上实现了ＯＯＦＬ到Ｃ＋＋的转换系统。从而提供了一种面向对象机制的描述工具。

一个C语言子集上的程序逻辑

在分离逻辑和C语言规范的基础上,设计一个C语言子集C3(C Code Certified)上的程序逻辑,其由操作语义、推导规则和可靠性证明组成.操作语义采用了小步的方式,为并发程序的验证留下了扩展的可能性.推导规则采用了扩展Hoare三元组的形式,易于程序员的理解,支持了更多的C语言特征.证明可靠性需要在语义上定义推导规则,本文采用了广为接受的直接定义方式,本文可靠性的证明在Coq中实现,并提供了一份可以通过机器自动检查的证明,保证了逻辑的可信度.证明实例展示了程序逻辑的可用性,程序验证工具可以直接使用C3的推导规则,简化验证的过程.

步进索引模型下的语义及其形式化

霍尔逻辑作为计算机程序的逻辑基础,可以用于描述一般程序的验证.分离逻辑作为霍尔逻辑的扩展,可以支持很多现代程序语言中的高阶特性.步进索引模型被用于定义自递归谓词.步进索引逻辑被广泛应用于各种基于交互式定理证明器的程序验证工具中,然而,基于步进索引逻辑的推理却比经典逻辑复杂、繁琐.事实上,也可以在步进索引模型上定义更加简洁清晰的、与“步数”无关的经典逻辑体系下的非步进索引程序语义.人们希望找到步进索引逻辑和非步进索引逻辑之间的关系,但发现两种逻辑并不等价.对实际的程序验证工作中涉及的命题进行归纳总结,找出它们共同的特征,给出关于程序状态的断言的约束条件;分别定义步进索引逻辑和非步进索引逻辑体系中断言的语义,并证明在该约束条件下两种语义的等价性;在Coq中,形式化以上所有定义和证明;最后,对未来值得关注的研究方向进行初步探讨.