用户设计意图的程序标注及其类型验证技术研究

随着软件规模日趋庞大、形态更加复杂，其可信性却越来越脆弱。传统的软件工程方法已经无法满足当今社会对软件可靠性和正确性的迫切需求，软件理论与方法学的研究面临重要的科学挑战，其中如何抽象地表述各种用户需求并与具体的程序代码相互印证成为构建可信赖软件的关键之一。本项目以面向对象软件的自动分析与验证为研究背景，探查用户的各种设计意图，分析用于显式声明软件行为特征和对象数据属性的常用程序标注及其语义，结合当前许可类型系统中类型规则和形式变换等理论成果，将形式化的许可类型作为桥梁，沟通抽象的程序标注和具体的程序代码，并进一步验证两者间的一致性，实现软件系统的正确性确认；在此基础上，设计并实现一个基于许可类型系统的程序分析和验证的原型系统。本项目旨在探索基于程序语言通用类型系统的形式化验证技术，为用户设计意图的准确勾勒、多程序标注的语义融合、许可类型系统的扩展和今后的工程应用奠定理论和技术基础。

本项目以面向对象软件的自动分析与验证为研究背景，探查用户的各种设计意图，分析用于显式声明软件行为特征和对象数据属性的常用程序标注及其语义，结合当前许可类型系统中类型规则和形式变换等理论成果，将形式化的许可类型作为桥梁，沟通抽象的程序标注和具体的程序代码，并进一步验证两者间的一致性，实现软件系统的正确性确认。在面向对象软件系统中，我们遴选了部分规范化的程序标注，这些标注显著的特点是能够归纳并抽象各种对象数据属性、软件行为特征和函数模块接口，显式声明用户的多种设计意图和软件属性。在此基础上，我们尝试综合理解多样化程序标注之间的内在关联，并通过形式化的许可类型对其进行语义表述；以基本对象为研究单位，讨论对象状态的分割和保护这一关键性的问题，通过探索许可类型系统中的类型规则和形式变换理论，正确定义静态的许可类型与动态的程序状态之间的一致性关联，分别在进展和保持定理的基础上证明了许可类型系统的安全性。此外，我们还进一步改进了基于传统数据流的程序分析和验证算法，以许可类型为媒介验证程序标注与程序代码的匹配性，从而沟通抽象用户设计意图和具体程序代码之间的障碍，实现了原型系统的设计并达到了预期的目标。本项目旨在探索基于程序语言通用类型系统的形式化验证技术，为用户设计意图的准确勾勒、多程序标注的语义融合、许可类型系统的扩展和今后的工程应用奠定理论和技术基础。