期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

目标独立的Prolog程序路径依赖分析语义 被引量：1

Goal-independent Semantics for Path Dependent Analysis of Prolog Programs
下载PDF
导出
摘要 在Prolog程序分析中,考虑程序的执行路径和非逻辑的cut操作可提高程序分析的精度。当前用于Prolog程序路径依赖分析的语义因依赖于程序执行的目标而不适合目标独立的程序分析。为此,本文采用了一种携带路径信息并允许cut操作的Prolog抽象语法,在此基础上给出了Prolog的操作语义和一种目标独立的标号树(LT)语义,并证明了LT语义相对于操作语义的正确性。LT语义可作为目标独立的Prolog程序路径依赖分析的基础。 Considering the execution path and cut operators of a Prolog program can improve the precision of program analysis. Known semantics for Prolog either makes use of limited amount of path information and hence leads to less precise analysis or is goal-dependent and therefore not suitable for goal-independent program analysis. This paper deals with the problems by proposing a goal-independent labeled tree semantics for Prolog with cut, which makes it possible to use call strings as context information to improve Prolog program analysis. This semantics is shown to be correct w. r. t the operational semantics presented in this paper.
作者 赵岭忠 古天龙 钱俊彦
机构地区 西安电子科技大学电子工程学院 桂林电子科技大学计算机与控制学院
出处 《计算机科学》 CSCD 北大核心 2008年第2期246-252,297,共8页 Computer Science
基金 国家自然科学基金(60563005,60663005) 广西青年科学基金(桂科青0728093,0542036)
关键词 程序分析 Prolog语义 目标独立 上下文信息 抽象解释 Program analysis, Prolog semantics, Goal-independence, Context information, Abstract interpretation
分类号 TP312 [自动化与计算机技术—计算机软件与理论] TP311 [自动化与计算机技术—计算机软件与理论]
  • 相关文献

参考文献24

  • 1Barbuti R, Codish M, Giacobazzi R, et al. Modeling Prolog control. Journal of Logic and Computation, 1993,3. 579-603.
  • 2Barbuti R, Codish M, Giacobazzi R, et al. Oracle Semantics for Prolog. In: Kirchner H, Levi G, eds. Algebraic and Logic Programming, Proceedings of the Third International Conference, Lecture Notes in Computer Science, vol 632, 1992. 100-114.
  • 3Barbuti R, Giacobazzi R, Levi G. 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.
  • 4Bossi A, Bugliesi M, Fabris M. Fixpoint Semantics for Prolog. In: Warren D S,ed. Proceedings of the Tenth International Conference on Logic Programming, Cambridge, MA.. MIP Prese, 1993. 374-389.
  • 5Borger E. A Logical Operational Semantics for Full Prolog. In: Borger E, Brining H K, Richter M M, eds. CSL' 89. Third Workshop on Computer Science Logic, Lecture Notes in ComputerScience, vol 440, 1990. 36-64.
  • 6Codish M, Dams D, Yardeni E. Bottom-up Abstract Interpretation of Logic Programs. Journal of Theoretical Computer Science, 1994,124:93-125.
  • 7Cousot P, Cousot R. Abstract Interpretation and Applications to Logic Programs. Journal of Logic Programming, 1992, 13 (23) : 103-179.
  • 8File G, Rossi S. Static Analysis of Prolog with Cut. LPAR, 1993. 134-145.
  • 9Fitting M. A Deterministic Prolog Fixpoint Semantics. Journal of Logic Programming, 1985,2(2) . 111-118.
  • 10Gabbrielli M, Levi G, Meo M C. Resultants Semantics for Prolog. Journal of Logic and Computation, 1996,6(4): 491-521.

同被引文献29

  • 1Comini M, Gori R, Levi G, et al. Abstract interpretation based verification of logic programs. Science of Computer Programming,2003,49(1/3) :89-123.
  • 2Cousot P. Automatic Verification by Abstract Interpretation// Fourth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI ' 03). LNCS, 2003 (2566):85 -108.
  • 3Comini M, Levi G, Vitiello G. Abstract Debugging of Logic Program//Proceedings of International Worksho Pon Meta-Programming in Logic (META), 1994 : 440-450.
  • 4Comini M, Levi G, Vitiello G. Efficient Detection of Incompleteness Errors in the Abstract Debugging of Logic Programs//Proceedings of AADEBUG. 1995:159-174.
  • 5Cousot P , Cousot R. An abstract interpretation - based framework for software watermarking. In Principles of Programming Languages 2003, POPL'03,2003 : 311- 324.
  • 6Zhao L,Gu T,Qian J. Goal-independent Semantics for Path Dependent Analysis of Prolog Programs//Proceedings of 1st IEEE IFI PInternational Symposium on Theoretical Aspects of Software Engineering (TASE 2007). 2007 : 261-270.
  • 7Cousot P. Abstract Interpretation Based Formal Methods and Future Challenges. LNCS,2000:138-156.
  • 8Clarke E M, Grumberg O, Peled D. Model Checking. Massachusetts: MIT Press, 1999.
  • 9Clarke E M, Grumberg O, Jha S, et al. Counterexample-guided Abstraction Refinement//Proceedings of Computer Aided Verification. 2000 : 154-169.
  • 10Lakhnech Y, Bensalem S, Berezin S, et al. Incremental Verification by Abstraction//Proceedings of TACAS 2001. LNCS, 2001,2031 : 98-112.

引证文献1

二级引证文献1

计算机科学
2008年 第2期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部