Institutional Repository
| PAR中泛型约束机制的设计与实现 | |
左正康
| |
| Major | 计算机软件与理论 |
| Supervisor | 薛锦云 |
| 2011-07 | |
| Degree Grantor | 中国科学院大学 |
| Degree Level | 博士 |
| Place of Degree Grantor | 北京 |
| Keyword | 泛型约束机制 Hoare公理语义 代数结构 Par Kleene泛型算法 |
| English Abstract | 泛型程序设计可以大幅度提高程序的可重用性、可靠性和开发效率，使建设软件构件工厂的理想得以实现。泛型约束机制可对泛型参数的合法性进行检测及验证，从而使得软件的可靠性和安全性得到显著提高。现有C++、Java主流语言泛型约束机制仅限于类型参数约束，且存在抽象程度不高，不易于形式验证等不足，严重限制了泛型程序设计方法的应用范围。本文研究PAR中泛型约束机制的设计与实现，基于代数结构语义和Hoare公理语义提出类型和操作约束机制在Apla中的设计方案，并建立PAR平台泛型约束匹配检测与验证模型及其相关算法。本论文的主要工作及研究成果：1． 在PAR中设计了抽象约束机制，提出了标准数据类型约束的代数结构描述方法、理论和实现技术，拓展了泛型程序设计数据类型约束的应用范围。2． 实现了操作约束功能，提出操作约束基于Hoare公理语义描述的方法，使用Dijkstra最弱前置谓词验证理论和PAR中循环不变式开发的新定义和新策略，借助Isabelle定理证明器，可验证实例操作参数与操作约束的匹配关系。3． 设计了PAR平台泛型约束匹配检测及验证模型及其相关算法，支持完善的模块化约束匹配自动检测及形式验证，并进一步设计了泛型约束机制在PAR平台的实现方案及其系统原型。4． 通过一个典型的基于闭半环代数结构约束的Kleene泛型算法展示了该类型约束机制的设计与实现方法；通过一个基于排序类操作约束的二分搜索算法和基于后序遍历类操作约束的中缀表达式求值算法展示了该操作约束机制的设计与实现方法。5． 实际使用效果表明该泛型约束机制可解决一系列复杂泛型约束问题，自动生成的C++程序的可靠性和安全性也得到显著提高。 |
| Subject | 程序设计及其语言 ; 软件工程 |
| Language | 英语 |
| Content Type | 学位论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/14886 |
| Collection | 基础软件与系统重点实验室 |
| Recommended Citation GB/T 7714 | 左正康. PAR中泛型约束机制的设计与实现[D]. 北京. 中国科学院大学,2011. |
| Files in This Item: | ||||||
| File Name/Size | DocType | Version | Access | License | ||
| 博士学位论文电子稿 - 左正康.pdf（1234KB） | 开放获取 | License | Application Full Text | |||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment