PAR中泛型约束机制的设计与实现

来源 :中国科学院大学 | 被引量 : 0次 | 上传用户:pengdou
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
泛型程序设计可以大幅度提高程序的可重用性、可靠性和开发效率,使建设软件构件工厂的理想得以实现。泛型约束机制可对泛型参数的合法性进行检测及验证,从而使得软件的可靠性和安全性得到显著提高。现有C++、Java主流语言泛型约束机制仅限于类型参数约束,且存在抽象程度不高,不易于形式验证等不足,严重限制了泛型程序设计方法的应用范围。本文研究PAR中泛型约束机制的设计与实现,基于代数结构语义和Hoare公理语义提出类型和操作约束机制在Apla中的设计方案,并建立PAR平台泛型约束匹配检测与验证模型及其相关算法。本论文的主要工作及研究成果:   1.在PAR中设计了抽象约束机制,提出了标准数据类型约束的代数结构描述方法、理论和实现技术,拓展了泛型程序设计数据类型约束的应用范围。   2.实现了操作约束功能,提出操作约束基于Hoare公理语义描述的方法,使用Dijkstra最弱前置谓词验证理论和PAR中循环不变式开发的新定义和新策略,借助Isabelle定理证明器,可验证实例操作参数与操作约束的匹配关系。   3.设计了PAR平台泛型约束匹配检测及验证模型及其相关算法,支持完善的模块化约束匹配自动检测及形式验证,并进一步设计了泛型约束机制在PAR平台的实现方案及其系统原型。   4.通过一个典型的基于闭半环代数结构约束的Kleene泛型算法展示了该类型约束机制的设计与实现方法;通过一个基于排序类操作约束的二分搜索算法和基于后序遍历类操作约束的中缀表达式求值算法展示了该操作约束机制的设计与实现方法。   5.实际使用效果表明该泛型约束机制可解决一系列复杂泛型约束问题,自动生成的C++程序的可靠性和安全性也得到显著提高。  
其他文献
随着信息技术的不断发展,信息化已经深入到了社会政治、经济、文化、生产、生活的各个领域,计算机网络已经成为人类生活、学习、工作等各方面不可缺少的工具。然而,伴随着网络在
在集成电路工艺以及微处理器性能需求的双重推动下,多核处理器逐渐取代单核处理器成为了市场的主流,微处理器的发展进入多核时代。当今大部分多核处理器采用共享存储的结构,各处
屏幕内容通常是指由电子设备的屏幕产生的视频或图像。随着计算机、平板电脑和智能手机等设备的迅速发展,屏幕内容在远程桌面、屏幕传输和云计算等应用中发挥着越来越重要的作
随着信息技术的发展,信息检索的作用日益凸显。特别是在图像检索领域,如何从海量的图像数据中快速、准确地寻找到我们期望的图像是一个十分重要且越来越热门的研究方向。基于内
近年来,随着塔式起重机在国内应用得越来越广泛,塔式起重机驾驶员的需求量在增加,同时安全事故发生率也在提高。在培训过程中,局限于一对一培训,培训内容有限,实际操作受现场条件限
词是计算语言学研究的重要对象,但从汉语词汇语义资源的建设情况来看,目前的汉语词义描述尚缺乏有效、客观、一致的辅助手段。因此,本文深入挖掘汉语的构词特点,尝试了一条经由汉
带参并发系统广泛存在于各类计算机系统的核心模块中,验证带参系统的正确性是形式验证领域中的一个热点问题。验证带参系统的难点在于:我们可以验证带参的一个很小规模的实例,
随着Internet的飞速发展,人们交流和获取信息的方式都发生了很大的变化,网络成了人们主要信息来源。政府网站作为电子政府的核心,逐渐成为了政府发布相关政策、法律、信息的主流
随着技术的发展,网络视频方兴未艾,而高清视频、3D视频等高质量的视频的提出和应用,对视频的存储、处理和传输提出了更高的要求。云计算服务的兴起,正好可以满足视频应用高存储和
随着集成电路的发展和电子产品的日新月异,微处理器的性能要求在不断的提升。当前单核微处理器体系结构研究主要通过挖掘指令间的并行度来提高微处理器的性能。流水线、乱序多