| 基于抽象解释的Prolog程序验证技术研究 |
| |
| 引用本文： | 赵岭忠,古天龙,蔡国永,钱俊彦.基于抽象解释的Prolog程序验证技术研究[J].计算机科学,2008,35(7):261-268. |
| |
| 作者姓名： | 赵岭忠 古天龙 蔡国永 钱俊彦 |
| |
| 作者单位： | 1. 西安电子科技大学电子工程学院,西安710071;桂林电子科技大学计算机与控制学院,桂林541004
2. 桂林电子科技大学计算机与控制学院,桂林541004 |
| |
| 基金项目： | 国家自然科学基金，广西青年科学基金 |
| |
| 摘 要： | 作为一种通用的语义近似理论,抽象解释已广泛应用于各类程序的形式化验证中.现有基于抽象解释的逻辑程序验证技术未涉及与程序点相关联的程序性质的验证,设计能够描述此类性质的逻辑程序具体语义和抽象语义是构造相应验证工具的关键.本文给出了一种基于抽象解释的Prolog程序验证方法,该方法采用了具有路径信息的Prolog语义及其抽象作为语义基础,因而可用于验证与程序点相关联的程序特性.本文例子表明了该验证方法的有效性.
|
| 关 键 词： | 抽象解释 程序验证 不动点语义 |
Abstract Interpretation Based Verification of Prolog Programs |
| |
| ZHAO Ling-zhong,GU Tian-long,CAI Guo-yong,QIAN Jun-yan.Abstract Interpretation Based Verification of Prolog Programs[J].Computer Science,2008,35(7):261-268. |
| |
| Authors: | ZHAO Ling-zhong GU Tian-long CAI Guo-yong QIAN Jun-yan |
| |
| Affiliation: | ZHAO Ling-zhong1,2 GU Tian-long2 CAI Guo-yong2 QIAN Jun-yan2(Electronic Engineering School,Xidian University,Xi'an 710071,China) 1 (School of Computer , Control,Guilin University of Electronic Technology,Guilin 541004,China) |
| |
| Abstract: | Abstract interpretation is a general theory of semantics approximation,which has been widely used in the verification of computer programs.Existing abstract interpretation based verification methods for logic programs do not deal with the properties associated with the program points.Based on our previous work on Prolog semantics,an abstract interpretation based verification method for Prolog programs is proposed in this paper,which makes use of a denotational semantics for Prolog that contains path informa... |
| |
| Keywords: | Prolog |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机科学》浏览原始摘要信息 |
|
点击此处可从《计算机科学》下载全文 |
|
