Analysis of Imperative Programs through Analysis of Constraint Logic Programs
Analysis of Imperative Programs through Analysis of Constraint Logic Programs
复制标题
DOI：
10.1007/3-540-49727-7_15
复制
发表时间：
1998-09
期刊：
影响因子：
--
通讯作者：
J. Peralta;J. Gallagher;Hüseyin Saglam
中科院分区：
文献类型：
--
作者：
J. Peralta;J. Gallagher;Hüseyin Saglam
本文提出了一种对命令式程序进行分析的方法。我们通过将语言语义写为声明性程序（在这里所示的方法中，是一个约束逻辑程序）来实现这一点。我们提出了一种有效的写作风格的操作语义适合分析，我们称之为单态小步骤语义。通过控制部分求值，我们能够生成剩余程序，其中命令语句和谓词之间的关系是直接的。然后，我们使用一个静态分析器的约束逻辑程序的剩余程序。分析结果通过程序点来解释，程序点将部分求值解释器中的谓词关联到其相应命令式程序中的语句。我们使用的分析器，使我们能够确定线性平等，不平等和不等关系的变量之间的程序，而无需用户提供的归纳断言或人类的互动。所提出的方法旨在作为一个框架，在任何命令式语言的程序分析。所需的工具是声明性语言的部分计算器和静态分析器。
In this paper a method is proposed for carrying out analysis of imperative programs. We achieve this by writing down the language semantics as a declarative program (a constraint logic program, in the approach shown here). We propose an effective style of writing operational semantics suitable for analysis which we callone-state small-stepsemantics. Through controlled partial evaluation we are able to generate residual programs where the relationship between imperative statements and predicates is straightforward. Then we use a static analyser for constraint logic programs on the residual program. The analysis results are interpreted through program points associating predicates in the partially evaluated interpreter to statements in its corresponding imperative program. We used an analyser that allows us to determine linear equality, inequality and disequality relations among the variables of a program without user-provided inductive assertions or human interaction. The proposed method intends to serve as a framework for the analysis of programs in any imperative language. The tools required are a partial evaluator and a static analyser for the declarative language.