| PAR中泛型约束机制的设计与实现 |
| 左正康
|
| 专业 | 计算机软件与理论
|
| 导师 | 薛锦云
|
| 2011-07
|
| 学位授予单位 | 中国科学院大学
|
| 学位 | 博士
|
| 学位授予地点 | 北京
|
| 关键词 | 泛型约束机制
Hoare公理语义
代数结构
Par
Kleene泛型算法
|
| 摘要 | 泛型程序设计可以大幅度提高程序的可重用性、可靠性和开发效率，使建设软件构件工厂的理想得以实现。泛型约束机制可对泛型参数的合法性进行检测及验证，从而使得软件的可靠性和安全性得到显著提高。现有C++、Java主流语言泛型约束机制仅限于类型参数约束，且存在抽象程度不高，不易于形式验证等不足，严重限制了泛型程序设计方法的应用范围。本文研究PAR中泛型约束机制的设计与实现，基于代数结构语义和Hoare公理语义提出类型和操作约束机制在Apla中的设计方案，并建立PAR平台泛型约束匹配检测与验证模型及其相关算法。本论文的主要工作及研究成果：1． 在PAR中设计了抽象约束机制，提出了标准数据类型约束的代数结构描述方法、理论和实现技术，拓展了泛型程序设计数据类型约束的应用范围。2． 实现了操作约束功能，提出操作约束基于Hoare公理语义描述的方法，使用Dijkstra最弱前置谓词验证理论和PAR中循环不变式开发的新定义和新策略，借助Isabelle定理证明器，可验证实例操作参数与操作约束的匹配关系。3． 设计了PAR平台泛型约束匹配检测及验证模型及其相关算法，支持完善的模块化约束匹配自动检测及形式验证，并进一步设计了泛型约束机制在PAR平台的实现方案及其系统原型。4． 通过一个典型的基于闭半环代数结构约束的Kleene泛型算法展示了该类型约束机制的设计与实现方法；通过一个基于排序类操作约束的二分搜索算法和基于后序遍历类操作约束的中缀表达式求值算法展示了该操作约束机制的设计与实现方法。5． 实际使用效果表明该泛型约束机制可解决一系列复杂泛型约束问题，自动生成的C++程序的可靠性和安全性也得到显著提高。 |
| 学科领域 | 程序设计及其语言
; 软件工程
|
| 语种 | 英语
|
| 内容类型 | 学位论文
|
| URI标识 | http://ir.iscas.ac.cn/handle/311060/14886
|
| 专题 | 基础软件与系统重点实验室
|
推荐引用方式
GB/T 7714 |
左正康. PAR中泛型约束机制的设计与实现[D]. 北京. 中国科学院大学,2011.
|
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论