泛型程序的规范和验证问题研究

本课题从泛型程序的规范表示和形式化验证的需要出发，目的是将一类软件表示为适用范围更广、互操作性更强的泛型形式，具体的软件可通过对泛型程序的参数实例化而获得, 且不降低运行效率；在构造性类型理论的框架下研究适合于表示泛型程序的规范，在正确性的证明过程中获取泛型程序的构造能力。课题的研究将针对目前模板元程序设计中的静态和动态语义问题，深入分析泛型函数式和泛型命令式程序设计（STL）的内在联系，用精确的概念表示一般的程序泛性；利用相关的数学方法（类型理论和范畴论）对泛型程序设计中的一些重要概念（抽象数据类型、参数化）进行刻画，使之建立在严格的数学基础之上；使程序的演算理论更加一般化,提出合理的静态检查机制和推导泛型程序的方法。从而有可能在新的形式化方法方面取得一些实质性的进展。

本项目从泛型程序的规范表示和形式化验证的需要出发，目的是将一类软件表示为适用范围更广、互操作性更强的泛型形式，具体的软件可通过对泛型程序的参数实例化而获得, 且不降低运行效率；在构造性类型理论的框架下研究适合于表示泛型程序的规范，在正确性的证明过程中获取泛型程序的构造能力。课题的研究将针对目前模板元程序设计中的静态和动态语义问题，深入分析泛型函数式和泛型命令式程序设计（STL）的内在联系，用精确的概念表示一般的程序泛性；利用相关的数学方法（类型理论和范畴论）对泛型程序设计中的一些重要概念（抽象数据类型、参数化）进行刻画，使之建立在严格的数学基础之上；使程序的演算理论更加一般化,提出合理的静态检查机制和推导泛型程序的方法。从而在新的形式化方法方面取得了一些实质性的进展。