基于约束的Prolog语义及其在Prolog程序测试、分析及验证中的应用研究

文摘

英文文摘

声明

第一章结论

1.1逻辑程序设计语言与Prolog概述

1.2逻辑程序设计和Prolog研究现状

1.3基于约束的逻辑程序和Prolog程序语义

1.4主要存在的问题及本文研究内容

1.5本文的结构

第二章基础知识：Prolog语言和抽象解释理论

2.1格与不动点理论

2.2 Prolog基础知识

2.2.1逻辑程序中的SLD-推导树

2.2.2 Prolog逻辑程序设计

2.2.3 Prolog语言中的切断(cut)操作

2.3抽象解释

2.3.1利用Galois连接对不动点语义进行近似

2.3.2利用widening/narrowing操作的抽象解释

2.4结束语

第三章目标独立的Prolog程序路径依赖分析语义

3.1引言

3.2 Prolog程序文法

3.3操作语义

3.4标号树语义

3.5标号树语义相对于操作语义的正确性

3.6 D-标号树语义

3.7相关工作

3.8结束语

第四章基于D-标号树语义的Prolog程序路径依赖分析

4.1引言

4.2语义域的设计

4.3路径依赖部分解语义

4.4路径依赖部分解语义的正确性

4.5路径依赖部分解语义的抽象

4.5.1路径信息的抽象

4.5.2基本约束和可见性约束的抽象

4.5.3抽象路径依赖部分解语义

4.6相关工作

4.7结束语

第五章基于D-标号树语义的Prolog程序验证

5.1引言

5.2基于路径依赖部分解语义的程序验证

5.3基于抽象语义的程序的验证

5.4相关工作

5.5结束语

第六章D-标号树语义的抽象-D-树语义

6.1 Prolog程序文法

6.2 D-树语义

6.3 D-树语义与D-标号树语义的关系

6.4计算解语义

6.5调用模式语义

6.6结束语

第七章基于计算解语义的逻辑程序测试和调试框架

7.1引言

7.2逻辑程序测试和调试框架

7.3测试和调试框架的实例化

7.3.1测试用例的生成

7.3.2性质规格

7.3.3一种综合的测试和调试算法

7.4实例分析

7.5相关工作

7.6结束语

第八章基于调用模式语义的PROLOG程序测试

8.1引言

8.2测试用例的生成

8.3基于近似调用模式语义的测试用例生成

8.4相关工作

8.5结束语

第九章调用模式语义在Prolog程序CPM测试中的应用

9.1 引言

9.2 CPM测试

9.3基于调用模式语义的测试帧更新

9.3.1用基本约束表示测试帧

9.3.2测试帧的更新

9.3.3基于近似调用模式语义的测试帧更新

9.3.4从更新后的测试帧产生测试用例

9.4相关工作

9.5结束语

第十章结论

致谢

参考文献

研究成果

附录