| 摘要: |
| 泛型程序设计可大幅提高程序的可重用性、可靠性和开发效率.泛型约束机制是对泛型参数进行形式描述,并对其合法性进行检测及验证,从而保证泛型程序的可靠性和安全性.分析总结多种主流语言的泛型约束特性,存在难以描述及验证基于动态语义的复杂约束需求问题,与完整实现GP尚有距离;以抽象程序设计语言Apla为宿主语言,提出了基于代数结构及公理语义的泛型约束方法,给出了基本数据类型、自定义抽象数据类型和子程序的3类泛型约束机制,拓展了泛型程序设计约束的应用范围.同时,支持静态语法和动态语义层约束,提高了泛型约束的精确度;借助Isabelle定理证明器,设计了泛型约束匹配检测和验证算法;进一步设计了泛型约束机制在PAR平台的实现方案及其系统原型.实验部分给出了该泛型约束机制描述、检测及验证一系列复杂泛型约束问题的全过程,自动生成的C++模板程序的可靠性和安全性得到显著提高. |
| 关键词: 泛型约束机制 Apla语言 代数结构 动态语义约束 安全性 |
| DOI：10.13328/j.cnki.jos.004628 |
| 分类号: |
| 基金项目:国家自然科学基金(61462039, 61020106009, 61363012, 61363013); 江西省自然科学基金(20142BAB217023, 20142BAB217026, 20142BAB207026); 江西省教育厅科技项目(GJJ14268) |
|
| Research on Generic Constraints of Apla |
|
ZUO Zheng-Kang1,2,3, XUE Jin-Yun1,2
|
|
1.State Key Laboratory of Computer Science, Institute of Software, The Chinese Academy of Sciences, Beijing 100190, China;2.Provincial Key Laboratory of High Performance Computing Technology (Jiangxi Normal University), Nanchang 330022, China;3.University of Chinese Academy of Sciences, Beijing 100049, China
|
| Abstract: |
| Generic programming has emerged as a paradigm for the development of highly reusable and safe software libraries. Generic constraints mechanism includes a collection of features for constraining generic parameters and verification of the validity of generic parameter instantiated, thereby guarantees dependability and safety of generic programs. This paper first reviews the current research status of generic constraints, exposing the difficulty of describing and verifying generic programs with dynamic semantic constraints. Based on a new description of generic constraints of Apla language, it then proposes three main types of generic constraints mechanism: constraints of basic data types, constraints of custom abstract data types and constraints of subroutines. Next, with the help of Isabelle theorem prover, the paper designs the generic constraints matching detection and validation algorithms and further gives the implementation scheme of generic constraints mechanism in PAR platform. It confirms that the proposed generic constraints mechanism can solve a series of complex generic constraints problems, and so markedly improves dependability and safety of generic programs. |
| Key words: generic constraints mechanism Apla language algebraic structure dynamic semantic constraint safety |
