基于代数结构及公理语义的泛型约束方法研究

结题报告

项目介绍

AI项目解读

基本信息

批准号：
61462039
项目类别：
地区科学基金项目
资助金额：
44.0万
负责人：
左正康
依托单位：
江西师范大学
学科分类：
F0203.软件理论、软件工程与服务
结题年份：
2018
批准年份：
2014
项目状态：
已结题
起止时间：
2015-01-01 至2018-12-31

项目参与者：
游珍；谢武平；江东明；卢家兴；胡珍新；吴莫海；岳巍；
关键词：
Hoare公理语义泛型约束代数结构 Apla PAR

项目摘要

Generic programming has emerged as a paradigm for the development of highly reusable and safe software libraries. Generic constraint mechanism can detect and verify the validity of generic parameter instantiated, thereby guarantee dependability and safety of generic programming. The research will study the current research situation of generic constraints. Based on a new description of generic constraints of Apla language,will propose generic constraint mechanism based on algebraic structures and axiomatic semantics. Then, with the help of Isabelle theorem prover, will design the generic constraints matching detection and validation algorithm. Further will design the implementation scheme of generic constraint mechanism in PAR platform and its prototype system. We expect that this generic constraint mechanism can solve a series of complex generic constraint problems, so should markedly improve dependability and safety of generic programming.

泛型程序设计(Generic Programming，简称 GP)可大幅提高程序的可重用性、可靠性和开发效率。泛型约束是对泛型参数的合法性进行检测及验证，已成为目前国内外研究的热点，对于保证泛型程序的可靠性和安全性有着重要的实际意义。本课题以抽象程序语言 Apla 为宿主语言，提出了基于代数结构及公理语义的泛型约束方法，同时支持语法和语义层约束，拓展了泛型程序设计约束的应用范围；拟设计泛型约束匹配检测和验证算法，支持完善的模块化约束匹配自动检测及语义匹配关系的形式验证；拟通过多个典型的泛型算法实例展示算法的设计与约束匹配验证过程；最后设计泛型约束机制在PAR平台的实现方案及系统原型。本课题的研究拟解决一系列复杂泛型约束问题，自动生成的 C++程序的可靠性和安全性可得到显著提高，为完整实现GP提供新思路和理论依据。

结项摘要

泛型程序设计可大幅提高程序的可重用性、可靠性和开发效率。泛型约束机制是对泛型参数进行形式描述，并对其合法性进行检测及验证，从而保证泛型程序的可靠性和安全性。分析总结多种主流语言的泛型约束特性，存在难以描述及验证基于动态语义的复杂约束需求问题，与完整实现GP 尚有距离。主要研究进展有：. 1.泛型及其约束机制分析。研究给出泛型程序设计及其约束的新定义，将泛型约束研究延伸到构件和服务参数化领域，重点讨论如何重用尽可能多的已部署服务。. 2.泛型约束机制在Apla 的设计。建立可以完备描述GP (Generic Programming)定义的Apla描述框架：包括数据类型和子程序约束。数据类型约束进一步细分基本数据类型约束和自定义抽象数据类型约束。使用一阶谓词逻辑公式的形式来刻画基本数据类型约束；基于代数结构来描述自定义抽象数据类型约束；基于Hoare公理语义的操作规约来描述子程序约束。. 3.约束匹配检测和验证算法。约束匹配检测基于PAR 平台完全自动完成；约束匹配验证则为部分自动化,需要手工推演出可验证的谓词逻辑公式,并验证其正确,部分逻辑公式借助Isabell定理证明器进行自动验证。. 4.泛型算法实例的设计及约束验证。基于三类泛型约束机制，选取典型泛型算法实例进行描述，并给出约束验证过程。. 5.泛型约束机制的PAR 平台实现。. 项目取得预期研究成果，共发表学术论文12篇（期刊论文6篇，会议论文6篇），其中2篇被SCIE收录（其中，JCR Q2期刊1篇，CCF推荐B类期刊1篇），5篇被EI收录，1篇被ISTP收录，北大中文核心期刊论文4篇（《软件学报》论文1篇）。项目负责人获科技部中国科学技术信息研究所颁发的“2016年度领跑者5000中国精品科技期刊顶尖学术论文奖”1项，获批中共江西省委组织部和江西省科学技术协会联合资助的2017年度“百人远航工程”1项；作为主编，出版科普性教材2部；围绕本课题研究内容，2015年至2018年间已培养硕士研究生7名（毕业3名，在读4名）。项目组成员多次赴国外参加国际学术会议。