本站原创
摘要：调试是发现和减少计算机程序或电子硬件中的错误或缺陷的有序历程。程序调试历程包括错误定位和代码修复两个阶段。近年来在代码修复方面提出了一些策略可以相对容易地发现错误缺陷的理由。现有代码修复主要有基于形式化规范和基于测试用例两种方式。但实际运用中很难直接对具有制约流结构的坃程序的复杂数据和制约联系进行推理。布尔程序是跟坃程序一样具有常规的制约流结构的命令式语言，它的所有变量只有布尔类型。布尔程序的特性使以其作为坃程序修复历程中间语言来实现代码修复是一个值得探讨的策略，现有探讨中对布尔程序进行修复方面尚未实现完全自动化修复。本论文在对布尔程序进行修复的策略上根据前人工作作了进一步的探讨和改善。本论文利用制约流结构对代码进行模拟运转构建出到达错误状态的错误路径以得到布尔修复。在构建错误路径时加入了更多的测试用例，使得能够覆盖的错误路径范围增大，由此对错误路径浅析后找到的布尔修复的准确性更高。本论文提出布尔程序修复的逆向转换策略，通过将得到的布尔程序修复逆向转换回坃程序的表达式，可以实现坃程序的整个修复历程完全自动化。得到布尔程序修复公式之后，首先根据在坃程序转换为布尔程序的历程中的变量映射联系将其转换为坃程序的表达式。转换之后对表达式的可满足性进行判断，当其可满足的时候才是坃程序的正确修复，可满足性判断不足可以归约到坓坍坔（可满足性模论述）不足。接着针对转换后坃程序的正确修复进行公式化简，将析取范式的修复通过修复子式内以及修复子式之间的联系进行化简得到有效最简的坃程序语句。根据本论文改善的修复策略和提出的逆向转换策略，设计并实现了一个布尔程序修复逆向转换工具，该工具输入已知错误位置的坃程序，将其转换为布尔程序进行修复，再把布尔程序的修复结果转换为坃程序的表达式，输出一个修复后坃程序。本论文采取了坔坃坁坓测试集来验证工具的正确性及有效性，实验结果显示该工具能够找到正确的修复结果且经过转换化简的修复结果贴近原程序的语义。关键词：代码修复论文布尔程序论文逆向转换论文可满足性模论述论文公式化简论文
摘要3-5
Abstract5-7
目录7-9
第1章 前言9-14
1.1 背景和作用9-11
1.2 探讨近况11-13
1.3 论文结构介绍13
1.4 本章小结13-14
第2章 布尔程序基础14-23
2.1 语法和语义14-16
2.2 布尔程序的模型检测16-18
2.3 布尔程序的构建18-21
2.4 本章小结21-23
第3章 布尔程序修复的逆向转换23-37
3.1 布尔程序的代码修复23-27
3.2 布尔修复的映射27-28
3.3 可满足性模论述归约28-31
3.4 修复公式化简31-36
3.5 本章小结36-37
第4章 逆向转换工具的设计与实现37-54
4.1 逆向转换系统架构37-38
4.2 逆向转换工具模块介绍38-39
4.3 布尔程序修复模块的设计与实现39-46
4.4 布尔修复逆向转换模块的设计与实现46-51
4.5 算法复杂度浅析51-52
4.6 本章小结52-54
第5章 布尔程序修复逆向转换工具测试实验54-61
5.1 TCAS测试用例集54-57
5.2 循环结构错误测试用例57-59
5.3 实验结果59
5.4 实验不足浅析59-60
5.5 本章小结60-61
第6章 结束语和进一步的工作61-63
6.1 结束语61
6.2 本论文不足及进一步的工作61-63