Constraint Based Prolog Semantics And Its Applications In The Testing, Analysis And Verification Of Prolog Programs

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.