Lecture Notes in Computer Science, 1998, Volume 1503/1998, 246-261, DOI: 10.1007/3-540-49727-7_15

Analysis of Imperative Programs through Analysis of Constraint Logic Programs

Julio C. Peralta, John P. Gallagher and Hüseyin Sağlam

View Related Documents

Abstract

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 call one-state small-step semantics. 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.

Keywords  Partial Evaluation - Constraint Logic Programming - Operational Semantics - Imperative Program Analysis

Fulltext Preview

Image of the first page of the fulltext document