文献类型：期刊文章

作　　者：左正康[1,2,3] 薛锦云[1,2]

机构地区：[1]中国科学院软件研究所计算机科学国家重点实验室,北京100190 [2]江西省高性能计算技术重点实验室(江西师范大学),江西南昌330022 [3]中国科学院大学,北京100049

出　　处：《软件学报》

基　　金：国家自然科学基金(61462039;61020106009;61363012;61363013);江西省自然科学基金(20142BAB217023;20142BAB217026;20142BAB207026);江西省教育厅科技项目(GJJ14268)

年　　份：2015

卷　　号：26

期　　号：6

起止页码：1340-1355

语　　种：中文

收录情况：AJ、BDHX、BDHX2014、CSA、CSA-PROQEUST、CSCD、CSCD2015_2016、EI(收录号：20152600981999)、IC、INSPEC、JST、MR、RCCSE、SCOPUS、ZGKJHX、ZMATH、核心刊

摘　　要：泛型程序设计可大幅提高程序的可重用性、可靠性和开发效率.泛型约束机制是对泛型参数进行形式描述,并对其合法性进行检测及验证,从而保证泛型程序的可靠性和安全性.分析总结多种主流语言的泛型约束特性,存在难以描述及验证基于动态语义的复杂约束需求问题,与完整实现GP尚有距离;以抽象程序设计语言Apla为宿主语言,提出了基于代数结构及公理语义的泛型约束方法,给出了基本数据类型、自定义抽象数据类型和子程序的3类泛型约束机制,拓展了泛型程序设计约束的应用范围.同时,支持静态语法和动态语义层约束,提高了泛型约束的精确度;借助Isabelle定理证明器,设计了泛型约束匹配检测和验证算法;进一步设计了泛型约束机制在PAR平台的实现方案及其系统原型.实验部分给出了该泛型约束机制描述、检测及验证一系列复杂泛型约束问题的全过程,自动生成的C++模板程序的可靠性和安全性得到显著提高.

关 键 词：泛型约束机制  APLA语言 代数结构 动态语义约束  安全性

分 类 号：TP311]