形状图理论的定理证明

发布时间：2017-11-02 13:07

  本文关键词：形状图理论的定理证明

  更多相关文章： 形状图逻辑 形状分析 程序验证 自动定理证明 循环不变式的推断

【摘要】：验证操作易变数据结构的指针程序仍面临很多挑战.数据结构中严重的指针别名显著地复杂化对操作这些结构的程序的推理.为分析和验证操作易变数据结构的指针程序,文中提出了形状图逻辑.形状图是描述程序中静态声明的堆指针变量和动态分配的结构体中指针域变量的指向的一种有向图,能准确表达指针的有效性和指针之间的相等性,可用于判断两个访问表达式是否是别名.形状图逻辑是Hoare逻辑的一种扩展,是一种直接将形状图作为程序中指针断言集的程序逻辑.该文研究形状图的等价理论和蕴含理论以及它们的判定方法和应用.首先,把形状图及其等价规则和蕴含规则分别类比为代数项及其等式规则和重写规则,像研究代数规范的理论那样来研究形状图理论.该文定义了形状图的语法理论和语义理论,定义了形状图重写系统及其终止性、局部合流性和合流性,然后得到基于形状图重写的形状图等价判定和蕴含判定的方法.其次,提出循环不变形状图和递归函数前后形状图的自动推断方法.借助形状图理论的判定方法,该文把一个基于抽象解释的推断循环不变式的一般方法改编成推断循环不变形状图的方法.由于计算终止的递归函数总有非递归的出口,可以先通过非递归路径得到函数的后形状图的初值,然后再在递归路径上迭代求解.从而,可以像推断循环不变形状图那样来推断递归函数的前后形状图.第三,参照Nelson-Oppen框架,提出形状图理论和整数理论组合的一种判定方法.对易变数据结构,除了关心数据结构各节点是否连成预定的形状外,往往还关心数据在这些节点间的排列等特性,它们不能脱离易变数据结构的形状特征而单独验证.为此,所提出的组合判定方法针对这类程序的验证条件的特点,利用程序分析阶段得到的形状图对验证条件的前件中的符号断言按形状图的节点分组;然后运用整数理论为各节点推导出尽可能多的性质;最后才交由定理证明器Z3去自动验证.这种方式有效地避免验证条件证明过程的不终止.基于形状图逻辑以及文中的工作,我们所开发的程序验证系统原型减轻了自动定理证明器的负担,并且能验证易变数据结构上较为复杂的程序,如有序循环双向链表、二叉排序树、伸展树、树堆、二叉平衡树和AA树的插入和删除函数.
【作者单位】： 中国科学技术大学计算机科学与技术学院;中国科学技术大学苏州研究院软件安全实验室;
【关键词】： 形状图逻辑 形状分析 程序验证 自动定理证明 循环不变式的推断
【基金】：国家“八六三”高技术研究发展计划项目基金(2012AA010901) 国家自然科学基金(61170018,61229201)资助~~
【分类号】：TP311.1
【正文快照】： 科学基金(61170018,61229201)资助.张昱,女,1972生,博士,副教授,中国计算机学会(CCF)高级会员,主要研究方向为程序设计语言的理论和实现技术、程序验证、确定性并行编程模型与运行时系统.E-mail:yuzhang@ustc.edu.cn.陈意云,男,1946年生,教授,博士生导师,中国计算机学会(CCF)

【相似文献】

中国期刊全文数据库 前10条

1 王洪君,任秀丽;基于对象形状特征的图象检索[J];松辽学刊(自然科学版);2001年03期

2 高飞;形状特征的表示[J];计算机辅助工程;1995年02期

3 王春河,张铁昌;面向集成化的形状特征分类与表示[J];航空学报;1996年02期

4 王春河,周济,张新访,张铁昌;凸起形状特征在集成过程中的处理技术[J];计算机辅助设计与图形学学报;1996年04期

5 张炜,杜晓荣,张蕊;形状特征的显示表达框架的构造[J];微机发展;1998年06期

6 贺双拾;辛玉林;倪友平;陈曾平;;基于灰度图形状特征的低分辨雷达架次判别[J];雷达科学与技术;2008年01期

7 廖凯宁;李志强;孙静;;基于形状特征描述算子的3D模型检索[J];计算机工程;2010年12期

8 高飞，，叶尚辉;形状特征的定义[J];计算机辅助工程;1994年01期

9 曹尚稳;两类形状特征的语义差及其操作互换性[J];系统工程与电子技术;1999年07期

10 赵书莲;宿晓华;;基于概念的形状分类与识别[J];电脑知识与技术;2009年06期

中国重要会议论文全文数据库 前6条

1 张世学;吴恩华;;基于形状特征与变形保持的动态模型简化[A];中国计算机图形学进展2008--第七届中国计算机图形学大会论文集[C];2008年

2 高剂斌;李裕梅;;基于复杂网络的图像形状特征提取及多特征融合方案探究[A];中国系统工程学会第十八届学术年会论文集——A12系统科学与系统工程理论在各个领域中的应用研究[C];2014年

3 胡帆;廖斌;薛巧平;;基于轮廓的形状特征提取方法[A];2011年通信与信息技术新进展——第八届中国通信学会学术年会论文集[C];2011年

4 路阳;董宏丽;;基于MATLAB实现水稻颗粒图像形状特征分析[A];黑龙江省计算机学会2007年学术交流年会论文集[C];2007年

5 李连;朱爱红;;基于形状的图像检索技术研究[A];’2004计算机应用技术交流会议论文集[C];2004年

6 甘俊英;赵向阳;张有为;;视觉语言特征—灰度轮廓权向量差分形状特征[A];图像 仿真 信息技术——第二届联合学术会议论文集[C];2002年

中国重要报纸全文数据库 前2条

1 程春;画面清新自然 寓意美好吉祥[N];中国集邮报;2014年

2 党耀武;给你一双“慧眼”　判读高空侦察照片[N];中国国防报;2002年

中国博士学位论文全文数据库 前10条

1 赵伟;自由形状特征的重用与抑制[D];浙江大学;2008年

2 王青;反求工程中基于变形的自由形状特征重构[D];浙江大学;2006年

3 陈飞;基于形状先验的同时分割与识别研究[D];浙江大学;2013年

4 柴伦绍;具有形变鲁棒性的形状特征研究及其在检索中的应用[D];北京邮电大学;2014年

5 桂江生;二维水果形状检测与分类算法研究[D];浙江大学;2007年

6 贾棋;形状不变特征提取及应用研究[D];大连理工大学;2014年

7 罗磊;形状分解和基于机器学习的图像检索技术研究[D];国防科学技术大学;2013年

8 王军伟;融合全局与局部信息的形状轮廓特征分析与匹配[D];华中科技大学;2012年

9 陈国栋;面向机器人的物体形状及姿态识别研究[D];哈尔滨工业大学;2011年

10 王淳;形状的部分结构解析和识别[D];华中科技大学;2014年

中国硕士学位论文全文数据库 前10条

1 王松鹤;2D形状中分支结构的检测[D];大连海事大学;2015年

2 周斌;基于图像形状特征量的计算机辅助肝硬化检测研究[D];广西大学;2015年

3 张倩;基于支持向量机的多特征交通标志识别的研究与实现[D];东北大学;2014年

4 李龙卓;基于形状特征的图像检索技术研究[D];青岛科技大学;2015年

5 江静宇;非刚体三维残缺模型的形状分类算法研究[D];北京交通大学;2016年

6 王璐;三维耳廓点云形状特征提取及匹配[D];辽宁师范大学;2015年

7 刘春爽;基于植物叶形状和叶脉的植物叶自动分类研究[D];浙江理工大学;2016年

8 顾华;基于形状特征的人脸分类研究[D];清华大学;2004年

9 李国琳;傅立叶描绘子对形状进行识别与检索[D];吉林大学;2005年

10 陈孝春;二维形状的描述和识别的研究[D];浙江大学;2006年

本文编号：1131663