基于约束的Prolog语义及其在Prolog程序测试、分析及验证中的应用研究
详细信息    本馆镜像全文|  推荐本文 |  |   获取CNKI官网全文
摘要
以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测试的有效性。为了说明本方法的有效性,给出了一种基于约束的近似调用模式语义,并举例演示了基于该语义的测试帧更新方法。
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.
引文
[1] R. Kowalski. Predicate Logic as Programming Language. In: Proceedings IFIP Congress, Stockholm, North Holland Publishing Co., 1974, pp. 569-574.
    [2] J. Jaffar and M.J. Maher. Constraint Logic Programming: A survey, Journal of Logic Programming, 1994,19-20: 503-581.
    [3] S. Muggleton and L. De Raedt. Inductive Logic Programming: Theory and Methods. Journal of Logic Programming, 1994,19/20: 629-679.
    [4] A. Kakas and M. Denecker. Abduction in logic programming. In: A. Kakas and F. Sadri, editors, Computational Logic: Logic Programming and Beyond. Part I, LNAI, 2002, 2407: 402-436.
    [5] R. Kowalski, F. Sadri. From Logic Programming towards Multi-agent Systems, Annals of Mathematics and Artificial Intelligence, 1999(3-4), 25: 391-419.
    [6] Y. Deville, Logic Programming: Systematic Program Development, Addison-Wesley Publishing Company, 1990.
    [7] T. Horvath, T. Gyim6thy, Z. Alexin and F. Kocsis. Interactive Diagnosis and Testing of Logic Programs. In: Proceedings of the Third Finnish-Estonian-Hungarian Symposium on Programming Languages and Software Tools Kaariku, Estonia, 1993, pp. 34-46.
    [8] G. K6kai, L. Harmath and T. Gyimothy. IDTS: a Tool for Debugging and Testing of Prolog Programs. In: Proceedings of LIRA'97, The 8th Conference on Logic and Computer Science, Novi Sad, Yugoslavia 1-4 September 1997,1997, pp. 103-110.
    [9] M. J. Balcer, W.M. Hasling and T. J. Ostrand. Automatic Generation of Test Script from Formal Test Specifications. In: Proceedings of the 3rd ACM Annual Symposium on Software Testing, Analysis, and Verification (TAV'89), 1989, pp. 210-218.
    [10]T.J. Ostrand and M.J. Balcer. The Category-Partition Method for Specifying and Generating Functional Tests. Communications of ACM, 1988, 31(6): 676-686.
    [11]F. Belli and O. Jack. Implementation-based Analysis and Testing of Prolog Programs. In: Proceedings of the 1993 ACM SIGSOFT International Symposium on Software Testing and Analysis, 1993, pp. 70-80.
    [12]F.Belli and O.Jack.A test coverage notion for logic programming,In:Proceedings of the Sixth International Symposium on Software Reliability Engineering,1995,pp.133-142.
    [13]F.Belli and O.Jack.Declarative paradigm of test coverage.Software Testing,Verification and Reliability,1998,8,15-47.
    [14]F.Belli and O.Jack.PROTest II,Testing Logic Programs,Technical report,1992/13,ADT,1992,October.
    [15]G.Luo,G.Bochmann,B.Sarikaya and M.Boyer.Control Flow Based Testing of Prolog Programs.In:Proceedings of the 3rd International Symposium on Software Reliability Engineering,1992,pp.104-113.
    [16]E.Y.Shapiro.Algorithmic Program Diagnosis.In:Proceedings of the Ninth Annual ACM Symposium on Principles of Programming Languages(POPL'82),1982,pp.299-308.
    [17]S.Y.Yan.Declarative Testing in Logic Programming.In:Proceedings of the Third Australian Software Engineering Conference,1987,pp.423-435.
    [18]M.Comini,G.Levi,G.Vitiello.Abstract Debugging of Logic Program.In:Proceedings of International Workshop on Meta-Prograrnming in Logic(META),1994,pp.440-450.
    [19]M.Comini,G.Levi,G.Vitiello.Efficient Detection of Incompleteness Errors in the Abstract Debugging of Logic Programs.In:Proceedings of AADEBUG 1995,1995,pp.159-174.
    [20]M.Comini,G.Levi and G.Vitiello.1995.Declarative diagnosis revisited.In:Proceedings of International Logic Programming Symposium,pp.275-287.
    [21]P.Cousot and R.Cousot.Abstract Interpretation Based Program Testing.In:Proceedings of the SSGRR 2000 Computer & eBusiness International Conference,Compact disk paper 248 and,L'Aquila,Rome,Italy,July 31-August 6,2000.
    [22]N.Dershowitz and Y.Lee.Deductive Debugging.In:Proceedings of the Fourth IEEE Symposium on Logic Programming,1987,pp.298-306.
    [23]M.Hermenegildo,G.Puebla,F.Bueno,P.Lopez-Garcia.Integrated program debugging,verification,and optimization using abstract interpretation(and the Ciao system preprocessor).Science of Computer Programming.2005,58(1-2):115-140.
    [24]L.Lu.and P.Greenfield.Logic Program Testing Based on Abstract Interpretation.In:Proceedings of the International Conference on Formal Methods in Programming and Their Applications.LNCS,1993,735:170-180.
    [25] P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, 1977, pp.238- 252.
    [26]P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In: Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'79), 1979, pp.269-282.
    [27] R. Barbuti, M. Codish, R. Giacobazzi and M. Maher. Oracle Semantics for Prolog. In: H. Kirchner and G. Levi editors, Algebraic and Logic Programming, Proceedings of the Third International Conference, LNCS, 1992, vol. 632, pp. 100-114.
    [28] G. File, and S. Rossi: Static Analysis of Prolog with Cut. In: Proceedings of LPAR 1993, 1993, pp. 134-145.
    [29]B.L. Charlier, S. Rossi, P.Van Hentenryck. Sequence-based Abstract Interpretation of Prolog, Theory and Practice of Logic Programming, 2002, 2(1): 25-84.
    [30]B. Le Charlier, S. Rossi and P. Van Hentenryck. An abstract Interpretation Framework Which Accurately Handles Prolog Search Rule and the Cut. In: M. Bruynooghe (Ed.), Proceedings of the 1994 International Symposium on Logic Programming, MIT Press, Cambridge, MA, 1994, pp. 157-171.
    [31]M. Falaschi, G. Levi, M. Martelli and C. Palamidessi. Declarative Modeling of the Operational Behavior of Logic Languages. Journal of Theoretical Computer Science, 69(3): 289-318,1989.
    [32]M. Codish, D. Dams and E. Yardeni. Bottom-up Abstract Interpretation of Logic Programs, Journal of Theoretical Computer Science, 1994,124: 93-125.
    [33]F. Spoto. Operational and Goal-independent Denotational Semantics for Prolog with Cut, The Journal of Logic Programming, 2000, 42: 1-46.
    [34]F. Spoto and Giorgio Levi. Abstract Interpretation of Prolog Programs. In: Proceedings of the Seventh International Conference on Algebraic Methodology and Software Technology, AMAST'98, LNCS, vol. 1548, Amazonia, Manaus, Brazil, January, Springer, Berlin, 1999, pp. 455-470.
    [35] G. Levi and D. Micciancio. Analysis of pure PROLOG programs. Technical Report D.WP1.2.2. M2, Esprit Project N. 6707 (ParForce), 1994.
    [36] G. Levi and F. Spoto. Accurate Analysis of Prolog with Cut. In: P. Lucio, M. Martelli, M. Navarro (Eds.), Proceedings APP1A-GULP-PRODE'96, 1996, pp. 481-492.
    [37]A.Bossi,M.Gabbrielli,G.Levi,and M.Martelli.The s-semantics approach:Theory and applications.Journal of Logic Programming,19-20:149-197,1994.
    [38]R.Barbuti,M.Codish,R.Giacobazzi and G.Levi.Modeling Prolog control,Journal of Logic and Computation,1993,3:579-603.
    [39]E.Borger.A Logical Operational Semantics for Full Prolog.In:E.Borger,H.Kleine Buning,M.M.Richter(Eds.),CSL'89.Third Workshop on Computer Science Logic,LNCS,vol.440,1990,pp.36-64.
    [40]M.Fitting.A Deterministic Proiog Fixpoint semantics,Journal of Logic Programming,1985,2(2),111-118.
    [41]M.Gabbrieili,G.Levi and M.C.Meo.Resultants Semantics for Prolog.Journal of Logic and Computation,1996,6(4):491-521.
    [42]C.Mellish.Abstract Interpretation of Prolog Programs,in S.Abramsky and.C.Hankin,editors,Abstract Interpretation of Declarative Languages,1987,pp.181-198.
    [43]A.Bossi,M.Bugliesi and M.Fabris.Fixpoint Semantics for Prolog.In:D.S.Warren(Ed.).In:Proceedings of the Tenth International Conference on Logic Programming,MIT Press,Cambridge,MA,1993,pp.374-389.
    [44]A.Cortesi and G.File.Abstract interpretation of logic programs:an abstract domain for groundness,sharing,freeness and coumpoundness analysis.In:Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics Based Program Manipulation,PEPM'91,SIGPLAN Notices,1991,26(1):52-61.
    [45]P.Cousot.Abstract Interpretation Based Formal Methods and Future Challenges.LNCS,2000,pp.138-156.
    [46]B.L.Charlier,C.Leclere,S.Rossi,A.Cortesi.Automated Verification of Prolog Programs.Journal of Logic Programming,1999,39(1-3):3-42.
    [47]M.Comini,R.God,G.Levi,P.Volpe.Abstract interpretation based verification of logic programs.Science of Computer Programming,2003,49(1-3):89-123.
    [48]G.Puebla,F.Bueno,M.Hermenegildo.An Assertion Language for Constraint Logic Programs.Analysis and Visualization Tools for Constraint Programming,2000,pp.23-62.
    [49]G.Puebla,F.Bueno,M.Hermenegildo.Combined Static and Dynamic Assertion-Based Debugging of Constraint Logic Programs.LOPSTR 1999:1999,pp.273-292.
    [50]P.Codognet and G.File.Computations,Abstractions and Constraints.In:Proceedings of the Fourth International Conference on Computer Languages.IEEE Press,1992.
    [51]R.Giacobazzi,S.K.Debray,G.Levi:A Generalized Semantics for Constraint Logic Programs.In:Proceedings of the International Conference on Fifth Generation Computer Systems,1992,pp.581-591.
    [52]R.Giacobazzi,G.Levi,S.K.Debray:Joining Abstract and Concrete Computations in Constraint Logic Programming.In:Proceedings of the Third International Conference on Algebraic Methodology and Software Technology(AMAST'93),1993,pp.111-127.
    [53]D.Boulanger and M.Bruynooghe and M.Denecker.Abstracting s-Semantics Using A Model-Theoretic Approach.In:Proceedings of 6th International Symposium Programming Language Implementation and Logic Programming (PLILP'94),LNCS,1994,pp.432-446.
    [54]P.Cousot.Automatic Verification by Abstract Interpretation.In:Proceedings of the Fourth International Conference on Verification,Model Checking and Abstract Interpretation(VMCAI'03).LNCS,2003,2566:85-108.
    [55]A.Tarski,A Lattice Theoretical Fixpoint Theorem and its Applications,Pacific Journal of Mathematics,1955,5:285-310.
    [56]陆钟万,面向计算机科学的数理逻辑(第二版),北京:科学出版社,2002.1.
    [57]石纯一,王家廞,数理逻辑与集合论(第二版),北京:清华大学出版社,2000.12.
    [58]M.H.van Emden and R.A.Kowalski.The semantics of predicate logic as a programming language,JACM,1976,23(4):733-742.
    [59]K.R.Apt and M.H.van Emden.Contributions to the theory of logic programming,Journal of the Association for Computing Machinery,1982,29(3):841-862.
    [60]K.L.Clark,Negation as Failure.In:Logic and Database pp.293-322.Plenum Press,New York,1978.
    [61]布拉特科(Bratko,I.)著,夏莹,陈群秀译,应用于人工智能的PROLOG程序设计,科学出版社,1991.8.
    [62]P.Cousot.Semantic Foundations of Program Analysis.In:Program Flow Analysis:Theory and Applications,S.S.Muchnick and N.D.Jones,editors,Chapter 10,pages 303-342.Prentice-Hall,Inc.,Englewood Cliffs,New Jersey,U.S.A.,1981.
    [63]P.Cousot and R.Cousot.Abstract Interpretation and Applications to Logic Programs,Journal of Logic Programming,1992,13(23):103-179.
    [64]P.Cousot and R.Cousot.Comparing the Galois connection and widening/narrowing approaches to abstract interpretation,invited paper.In:Proceedings of the Fourth International Symposium on Programming Language Implementation and Logic Programming,PLILP'92,LNCS,1992,631:269-295.
    [65]L.Henkin,and J.D.Monk,A.Tarski.Cylindric Algebras.Parts Ⅰ and Ⅱ,North-Holland,Amsterdam,1971.
    [66]G.Ferrand.The Notions of Symptom and Error in Declarative Diagnosis of Logic Programs.In:Proceedings of the First International Workshop on Automated and Algorithmic Debugging,LNCS,1993,749:40-57.
    [67]J.W.Lloyd.Declarative error diagnosis.New Generation Computing,1987,5(2):133-154.
    [68]L.Lu.A Generic Declarative Diagnoser for Normal Logic Programs.LNAI,1994,822:290-304.
    [69]L.Lu.Use of Correctness Assertions in Declarative Diagnosis.In:Proceedings of the 2005 ACM symposium on Applied computing,2005,pp.1404-1408.
    [70]J.Silva.Algorithmic Debugging Strategies.Proceedings of International Symposium on Logic-based Program Synthesis and Transformation(LOPSTR 2006),2006,pp.134-140.
    [71]J.Silva and O.Chitil.Combining Algorithmic Debugging and Program Slicing.In:Proceedings of the 8th ACM SIGPLAN symposium on Principles and practice of declarative programming,2006,pp.157-166.
    [72]M.Dincbas,P.V.Hentenryck,H.Simonis and A.Aggoun.The Constraint Logic Programming Language CHIP.In:Proceedings of the International Conference on Fifth Generation Computer Systems,1988,pp.693-702.
    [73]Colmerauer A.An Introduction to PROLOG-Ⅲ.Communications of the ACM,1990,33(7):69-90.
    [74]T.Y.Chen,Pak-Lok Pooh and T.H.Tse.A Choice Relation Framework for Supporting Category-Partition Test Case Generation,IEEE Transactions on Software Engineering,2003,29(7):577-593.
    [75]M.Ducasse and J.Noye.Logic Programming Environments:Dynamic Program Analysis and Debugging.Journal of Logic programming,1994,19-20:351-384.
    [76]M.Gabbrielli,G.Levi and M.C.Meo.Observable Behaviors and Equivalences of Logic Programs.Information and Computation,1995,122(1):1-29.
    [77]R.Patton.Software Testing,Second Edition,Pearson Education,Inc,2006.
    [78] S. J. Zeil and C. Wild. A Knowledge Base for Software Test Refinement. In: Proceedings of 8th Knowledge-Based Software Engineering Conference, 1993, pp. 50-57.
    [79] P. Stocks and D. Carrington. A Framework for Specification-Based Testing. IEEE Transactions on Software Engineering, 1996, 22 (11): 777-793.
    
    [80]N. Amla and P. Ammann. Using Z Specifications in Category-Partition Testing. In: Proceedings of 7th Annual IEEE Conference on Computer Assurance (COMPASS '92), 1992, pp. 3-10.
    [81] P. Ammann and A. J. Offutt. Using Formal Methods to Derive Test Frames in Category Partition Testing. In: Proceedings of the Ninth Annual Conference on Computer Assurance (COMPASS'94), 1994, pp. 69-80.
    [82]A. J. Offutt and A. Irvine. Testing Object-Oriented Software Using the Category-Partition Method. In: Proceedings of 17th International Conference on Technology of Object-Oriented Languages and Systems (TOOLS 17), 1995, pp. 293-304.
    [83]M. Gabbrielli and R. Giacobazzi. Goal Independency and Call Patterns in the Analysis of Logic Programs. In: Proceedings of the Ninth ACM Symposium on Applied Computing, 1994, pp. 394-399.
    [84]M. Gabbrielli and M.C. Meo. Fixpoint Semantics for Partial Computed Answer Substitutions and Call Patterns. LNCS, 1992, 632: 84-99.
    [85]R. Barbuti, R. Giacobazzi and G. Levi. A General Framework for Semantics-Based Bottom-Up Abstract Interpretation of Logic Programs, ACM Transactions on Programming Languages and Systems, 1993,15(1): 133-181.
    [86]J. M. Howe and A. King. Efficient Groundness Analysis in Prolog. Theory and Practice of Logic Programming, 2003, 3(1): 95-124.
    [87] K. Marriott and H. Sndergaard. Precise and Efficient Groundness Analysis for Logic Programs. ACM Letters on Programming Languages and Systems, 1993, 2(1-4): 181-196.
    [88]P. Volpe. 2001. A First-order Language for Expressing Sharing and Type Properties of Logic Programs. Science of Computer Programming, 39(1): 125-148.
    [89] F. Nielson, H. R. Nielson, C. Hankin. Principles of Program Analysis. Springer-Verlag Heidelberg, 1999.
    [90] K. Marriott, H. S(?)ndergaard and Neil D. Jones. Denotational abstract interpretation of logic programs, ACM Transactions on Programming Languages and Systems (TOPLAS), 1994,16(3): 607 - 648.
    [91]H.Winsborough.Path-Dependent Reachability Analysis for Multiple Specialization.In:Proceedings of the North American Conference on Logic Programming,1989,pp.133-153.
    [92]H.Sφdergaard.An application of abstract interpretation of logic programs:occur check reduction.In:Proceedings ESOP'86,LNCS 213,pages 327-338.Springer-Verlag,Berlin,Germany,1986.
    [93]U.Nilsson.Systematic semantic approximations of logic programs.In:P.Deransart and J.Maluszynski,editors,Proceedings of the International Workshop PLILP' 90,Programming Language Implementation and Logic Programming,LNCS 456,pp.293-306.Springer-Verlag,Berlin,Germany,August 20-22,1990.
    [94]M.Bruynooghe,G.Janssens,A.Callebaut,and B.Demoen,Abstract interpretation:towards the global optimisation of PROLOG programs.In:Proceedings of 1987 Symposium on Logic Programming,1987,pp.192-204.
    [95]E.Yardeni and E.Shapiro.A type system for logic programs,in E.Shapiro,editor,Concurrent Prolog,Collected Papers,chapter 28,1987,pp.211-244.
    [96]L.Lu.Path Dependent Analysis of Logic Programs.In:Proceedings of ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation(PEPM '02),2002,pp.63-74.
    [97]P.Cousot and R.Cousot.An abstract interpretation-based framework for software watermarking,in Proceedings of POPL'03,2003,pp.311-324.
    [98]E.M.Clarke,O.Grumberg,D.Peled.Model Checking.Massachusetts:MIT Press,1999
    [99]E.M.Clarke,O.Grumberg,S.Jha,Y.Lu,H.Veith.Counterexample-guided Abstraction Refinement.In:Proceedings of Computer Aided Verification,2000,pp.154-169.
    [100]Y.Lakhnech,S.Bensalem,S.Berezin,S.Owre.Incremental Verification by Abstraction.In:Proceedings of TACAS 2001,LNCS,2001,2031:98-112.
    [101]P.Deransart.Proof methods of declarative properties of definite programs.Theoretical Computer Science,1993,118:99-166.
    [102]C.Hogger.Introduction to Logic Programming.Academic London,1984.
    [103]A.Bossi and N.Cocco.Verifying correctness of logic programs.In:Proceedings of Tapsoft'89,1989,pp.96-110.
    [104]K.R.Apt and E.Marchiori.Reasoning about Prolog Programs:From Modes Through Types to Assertions.Formal Aspects of Computing,1994,6(6A):743-764.
    [105]W.Drabent.It is declarative.In:A.Bossi,editor,ILPS post-conference Workshop on Verification,Model Checking and Abstract Interpretation,Port Jefferson,Long Island N.Y.,USA,1997.
    [106]赵岭忠,古天龙,钱俊彦.目标独立的Prolog程序路径依赖分析语义,计算机科学,2008第2期发表.
    [107]L.Zhao,T.Gu and J.Qian.Goal-independent Semantics for Path Dependent Analysis of Prolog Programs.In:Proceedings of 1st IEEE & IFIP International Symposium on Theoretical Aspects of Software Engineering(TASE 2007),2007,pp.261-270.
    [108]G.File,R.Giacobazzi,F.Ranzato.A Unifying View of Abstract Domain Design.ACM Computing Surveys,1996,28(2):333-336.
    [109]R.Giacobazzi,F.Ranzato,F.Seozzari.Making abstract interpretations complete.Journal of ACM,2000,47(2):361-416.
    [110]R.Giacobzzi,F.Ranzato,F.Seozzari.Making abstract domains condensing.ACM Transactions on Computational Logic,2005,6(1):33-60.
    [111]Yi-Dong Shen,Li-Yan Yuan,Jia-Huai You,Neng-Fa Zhou.Linear Tabulated Resolution Based on Prolog Control Strategy.Theory and Practice of Logic Programming,2001,1(1):71-103.
    [112]Yi-Dong Shen,Li-Yan Yuan,Jia-Huai You.SLT-resolution for the well-founded semantics.Journal of Automated Reasoning,2002,28(1):53-97.
    [113]Yi-Dong Shen,Jia-Huai You,Li-Yan Yuan.Enhancing global SLS-resolution with loop cutting and tabling mechanisms.Theoretical Computer Science,2004,328(3):271-287.
    [114]V.Dahl,I.Niemela(Eds.):Proceedings of the 23rd International Conference on Logic Programming,ICLP 2007,Porto,Portugal,September 8-13,2007.Lecture Notes in Computer Science,4670,Springer 2007.
    [115]M.Balduccini,M.Gelfond.Diagnostic reasoning with A-Prolog.Theory and Practice of Logic Programming,2003,3(4-5):425-61.
    [116]M.Gelfond,N.Leone.Logic programming and knowledge representation-the A-Prolog perspective.Artificial Intelligence,2002,138(1-2):3-38.
    [117]H.Vandecasteele,G.Janssens.An open ended tree[data structure in Prolog programs].Theory and Practice of Logic Programming,2003,3(3):377-85.
    [118]J.H.Andrews.The witness properties and the semantics of the Prolog cut.Theory and Practice of Logic Programming,2003,3(1):1-59.
    [119]E.Pontelli,K.Villaverde,Hai-Feng Guo,G.Gupta.PALS:Efficient or-parallel execution of prolog on Beowulf clusters.Theory and Practice of Logic Programming,2007,7(6):633-695.
    [120]G.Xirogiannis,H.Taylor.PAN:a portable,parallel prolog:its design,realisation and performance.New Generation Computing,2002,20(4):373-99.
    [121]G.Gupta,E.Pontelli,Khayri A.M.Ali;M.Carlsson,M.V.Hermenegildo.Parallel Execution of Prolog Programs:A Survey.ACM Transactions on Programming Languages and Systems,2001,23(4):472-602.
    [122]Z.Huang,C.Sun,A.Sattar.Handling side-effects and cuts with selective recomputation in parallel Prolog.Future Generation Computer Systems,2000,17(3):227-45.
    [123]F.Silva,P.Watson.Or-parallel Prolog on a distributed memory architecture.Journal of Logic Programming,v 43,n 2,May 2000,p 173-85.
    [124]L.Araujo.Some essential side-effects of Prolog on a distributed implementation.Computers and Artificial Intelligence,2000,19(2):147-67.
    [125]A.S.Mohamed,R.Galal,I.Khalil,K.Sobh,M.Selim.DISPO:distributed multi-threaded execution of Prolog programs.International Journal of Computers & Applications,2000,22(2):100-108
    [126]R.Vandeginste,B.Demoen.Incremental copying garbage collection for WAM-based Prolog systems Theory and Practice of Logic Programming,2007,7(5):505-536.
    [127]R.Lopes,L.F.Castro,V.S.Costa.From simulation to practice:Cache performance study of a prolog system.ACM SIGPLAN Notices,2003,38 SUPPL.(2):56-64.
    [128]M.Fico.Theory of local register allocation for Prolog clauses.Ⅱ.Computers and Artificial Intelligence,2000,19(1):79-103.
    [129]K.Djelloul,Thi-Bich-Hanh Dao,T.Fruehwirth.Toward a first-order extension of Prolog's unification using CHR:A CHR first-order constraint solver over finite or infinite trees.Proceedings of the 2007 ACM Symposium on Applied Computing,2007,pp.58-64.
    [130]萧镇,韩国新,龚育昌,赵振西.Prolog抽象机及运行模型研究.计算机研究与发展,1999,36(11):1402-1408.
    [131]V.S.Costa,K.F.Sagonas,R.Lopes.Demand-Driven Indexing of Prolog Clauses.Proceedings of the 23rd International Conference on Logic Programming (ICLP 2007),Lecture Notes in Computer Science,2007,4670,pp.395-409.
    [132]M.Wermelinger.A Prolog toolkit for formal languages and automata.SIGCSE Bulletin,2005,37(3):330-334.
    [133]J.Esch.Prolog to data-hiding codes.Proceedings of the IEEE,2005,93(12):2081-2082.
    [134]H.Falk.Prolog to:Active harmonic filters.Proceedings of the IEEE,2005,93(12):2127.
    [135]R.O'Donnell.Prolog to reactive power compensation technologies.Proceedings of the IEEE,2005,93(12):2142-2143.
    [136]Chia-Chu Chiang.Automated rapid prototyping of TUG specifications using Prolog.Information and Software Technology,2004,46(13):857-73.
    [137]A.Cordon-Franeo,M.A.Gutierrez-Naranjo,M.J.Perez-Jimenez,F.Sancho-Caparrini.Prolog simulator for deterministic P systems with active membranes.New Generation Computing,2004,22(4):349-363.
    [138]J.L.Sierra,A.Fernandez-Valmayor.A Prolog Framework for the Rapid Prototyping of Language Processors with Attribute Grammars.Electronic Notes in Theoretical Computer Science,2006,164(2):19-36.
    [139]G.K.Palsjikar.Simulation of Petri nets in Prolog:modeling dynamic system behavior.PC AI,2001,15(3):43-45.
    [140]L.Pant.Developing intelligent systems with Java and Prolog.2000,Java Report,5(5):22-32.
    [141]E.Denti,A.Omicini,A.Ricci.Multi-paradigm Java-Prolog integration in tuProlog.Science of Computer Programming,2005,57(2):217-50.
    [142]A.Amandi,M.Campo,A.Zunino.JavaLog:A framework-based integration of Java and Prolog for agent-oriented programming Computer Languages,Systems and Structures,2005,31(1):17-33.
    [143]A.Csenki.Rotations in the plane and Prolog.Science of Computer Programming,2007,66(2):154-161.
    [144]A.Csenki.Enigma 1225:Prolog-assisted solution of a puzzle using discrete mathematics.Computers and Mathematics with Applications,2006,52(3-4):383-400.
    [145]S.W.Loke.Declarative programming of integrated peer-to-peer and Web based systems:the case of Prolog.Journal of Systems and Software,2006,79(4):523-536.
    [146]L.Hunyadi.Prosper:A Framework for Extending Prolog Applications with a Web Interface.Proceedings of the 23rd International Conference on Logic Programming(ICLP 2007),Lecture Notes in Computer Science,2007,4670,pp.432-433.
    [147]A.M.Andrew.The commercial use of PROLOG.Kybernetes,2005,34(5):599-601.
    [148]申晓勇,雷英杰,王坚.基于Visual Prolog 6.3内核的专家系统实现,计算机技术与发展,2006,16(12):91-93.
    [149]徐彤,雷英杰,谢波,李松.Visual Prolog确定性管理机制剖析.计算机工程,2005,31(22):192-193.
    [150]周炎涛.PROLOG语言在数据挖掘Apriori算法中的实现.计算机工程与应用,2003,39(21):195-196.
    [151]赵爽,文瑾,施心陵.基于逻辑描述的决策树算法及其Prolog实现.云南大学学报:自然科学版,2005年27卷3期:211-215.
    [152]吉张媛,何华灿.模糊Prolog系统.计算机技术与发展,2006,16(2):123-125.
    [153]蒋志华,姜云飞.一种构造Prolog程序子句本体的方法.东南大学学报:英文版,2006,22(3):357-360.
    [154]王啸澜,赵致琢,李慧琪.Prolog语言与G6del语言中元程序设计方法的研究.厦门大学学报:自然科学版,2005,44(B06):247-250.
    [155]余金山.Prolog的语义保持变换.华侨大学学报:自然科学版,2001,2(1):100-104.
    [156]董玉萍.从PROLOG到PASCAL的程序转换.医学信息:医学与计算机应用,2003,16(10):561-563.

© 2004-2018 中国地质图书馆版权所有 京ICP备05064691号 京公网安备11010802017129号

地址:北京市海淀区学院路29号 邮编:100083

电话:办公室:(+86 10)66554848;文献借阅、咨询服务、科技查新:66554700