Arrow Research search
Back to LOPSTR

LOPSTR 2000

Imperative Program Specialisation: An Approach Using CLP

Conference Paper Analysis and Specialisation Formal Methods ยท Logic in Computer Science

Abstract

Abstract The semantics of an imperative programming language can be expressed as a program in a declarative constraint language. Not only does this render the semantics executable, but it opens up the possibility of applying to imperative languages the advances made in program analysis and transformation of declarative languages. We propose a method for carrying out partial evaluation of imperative programs, using partial evaluation in a declarative language, but returning the results in the syntax of the imperative program which is to be partially evaluated. The approach uses a special form of the semantics and program points to aid partial evaluation. The partially evaluated semantics program is represented as a labelled directed graph. An algorithm for reconstructing an imperative program from the graph and the residual program is presented. Constraints provide a means through which information is propagated inside both branches of a conditional, the body of a loop, and along def-use chains in the program. The method provides a framework for constructing a partial evaluator for any imperative programming language, by writing down its semantics as a declarative program (a constraint logic program, in the approach shown here).

Authors

Keywords

No keywords are indexed for this paper.

Context

Venue
International Symposium on Logic-Based Program Synthesis and Transformation
Archive span
1990-2025
Indexed papers
560
Paper id
519462142250827849
v2026.09.13