以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测试的有效性。为了说明本方法的有效性,给出了一种基于约束的近似调用模式语义,并举例演示了基于该语义的测试帧更新方法。