【作者】 赵岭忠；

【导师】 古天龙；

【作者基本信息】 西安电子科技大学 ， 模式识别与智能系统， 2007， 博士

【摘要】 以Prolog为代表的逻辑程序设计(LP)语言是一类重要的人工智能应用语言。其主要特点是问题描述和问题求解过程的分离。如何利用LP语言开发正确可靠的应用软件系统是逻辑程序设计研究的热点之一。本文以基于约束的Prolog形式语义和抽象解释理论为工具,对Prolog程序测试、调试、分析和验证过程中遇到的问题进行了探索和研究。课题得到了国家自然科学基金和广西科学基金的资助。论文主要研究结果包括:1)针对现有Prolog语义在描述与程序点相关程序性质上的不足,给出了一种携带路径信息并允许cut操作的Prolog抽象语法,并基于此给出了一种Prolog操作语义、目标独立的标号树语义和D-标号树语义,证明了标号树语义和D-标号树语义相对于操作语义的正确性。2)作为D-标号树语义的抽象,给出了一种独立于目标的Prolog路径依赖部分解语义。由该语义可计算任意目标的执行过程中在每一个程序点获得的部分解。利用现有的语义抽象技术该语义可以抽象为一个有限可计算的语义,从而可进行目标独立的Prolog程序分析。3)把Prolog路径依赖部分解语义用于基于抽象解释的Prolog程序验证,给出了一种验证与Prolog程序点相关联程序性质的方法。本文例子表明了该验证方法的有效性。4)给出了一种综合的逻辑程序测试和调试框架,基于该框架的逻辑程序测试和调试算法可减少对调试过程不必要的调用,从而提高软件开发的效率。在一种基于约束的Prolog计算解语义(该语义可视为D-标号树语义的抽象)的基础上,给出了该框架的一个实例,说明了该框架的应用。5)以Prolog程序控制流图的隐式表示为基础,给出了一种基于调用模式语义的Prolog程序测试用例生成方法。所使用的调用模式语义可视为D-标号树语义的另一抽象。与由于显式控制流图规模庞大而不得不采用不完整控制流图的Prolog程序测试相比,隐式表示中包含完整的控制流信息,且允许测试人员通过适当的语义抽象灵活地适应测试的要求。6)研究了调用模式语义在Prolog程序CPM(Category Partitioning Method)测试中的应用,给出了一种对CPM测试帧进行缩减和精化的新途径。与程序实现相关的知识被用于CPM测试帧的更新。相对于本文关心的程序错误的检测而言,该更新保持了传统CPM测试的有效性。为了说明本方法的有效性,给出了一种基于约束的近似调用模式语义,并举例演示了基于该语义的测试帧更新方法。更多还原

【Abstract】 Logic programming (LP) is an important programming paradigm that has multiple applications in the areas of artificial intelligence. LP languages, of which Prolog is a representative, feature the separation of the description of a problem and the way to solve the problem. One of the focuses in the research of LP is on how to develop correct and reliable software systems using LP languages. We studied the problems arising in the software development with Prolog, in particular, the problems in the testing, debugging, analysis and verification of Prolog programs. In doing so, the framework of abstract interpretation and a class of constraint-based Prolog semantics are used as the theoretical tools. This work was supported by the National Natural Science Foundation of China (grant No.60563005, 60663005), and the Natural Science Foundation of GuangXi (grant No. GuiKeQing 0728093 and GuiKeQing 0542036).The contributions of this paper are as follows.1) Considering the execution path and cut operators of Prolog program can improve the precision of program analysis. Known semantics for Prolog that explicitly or implicitly considers execution paths as context are goal-dependent and therefore not suitable for goal-independent program analysis. This paper deals with the problem by proposing an operational semantics and a goal-independent labeled tree semantics, both of which are capable of dealing with cut operators. The latter is shown to be correct w.r.t. the former. In order to make the semantics suitable for abstract interpretation, a decorated labeled tree (D-labeled tree) semantics is proposed which is shown to be correct w.r.t. the labeled tree semantics.2) The application of the D-labeled tree semantics in program analysis is investigated. As an abstraction of the semantics, we proposed a goal-independent denotational semantics for Prolog with cut, called path dependent partial answer semantics, from which we can compute for each program point the set of partially computed answers obtained in the execution of any goal. With existing abstraction techniques this semantics is abstracted into a finitely computable semantics that can be used for goal-independent Prolog program analysis.3) Existing abstract interpretation based verification methods for logic programs do not deal with the properties associated with the program points. An abstract interpretation based verification method for Prolog programs is proposed in this paper, which makes use of the path dependent partial answer semantics proposed in 2). Since the semantics is capable of describing program properties associated with program points, it’s natural for our verification method to be able to verify such a class of properties. The applicability of our method is exemplified in this paper.4) An integrated testing and debugging framework is proposed for logic programs. The framework is designed with the aim to reduce unnecessary calls to the debugging procedure for logic programming languages, and hence to improve the efficiency of software development. With a constraint-based computed answer semantics for Prolog, the framework is instantiated to a novel testing and debugging algorithm whose applicability is shown in this paper.5) Traditional control flow graph (CFG) based testing methods for Prolog use explicit representation of CFG. Since the CFG for Prolog program is usually extremely large even for small programs, these methods have to be satisfied with using an incomplete representation of CFG of programs. An alternative way to generate test cases for a Prolog program is to view the call patterns of the procedures in the program as an implicit representation of the CFG of the program. This paper explores the idea by proposing a call patterns semantics based test case generation method. Compared with traditional CFG-based test case generation, the method is more flexible and can be easily adapted to meet the requirements of a tester expressed by the approximation of the call patterns semantics we use.6) Category Partition Method (CPM) is a general approach to specification-based program testing, where test frame reduction and refinement are two important issues. We propose a novel method for updating test frames generated by traditional CPM testing of Prolog programs, in which implementation related knowledge is used as an alternative to user-provided information for reducing and refining CPM test frames. Our test frame updating method preserves the effectiveness of CPM testing w.r.t the detection of faults we care. In order to show the applicability of our method an approximation call patterns semantics is proposed, and the test frame updating on the semantics is illustrated by an example.更多还原