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

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

项目编号： No.61462039

项目类型： 地区科学基金项目

立项/批准年度： 2015

项目学科： 自动化技术、计算机技术

项目作者： 左正康

作者单位： 江西师范大学

项目金额： 44万元

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

中文关键词： 泛型约束；代数结构；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 Constraints;Algebraic Structures;Hoare Axiomatic Semantics;Apla;PAR