Browse Reports

The semantics of an imperative programming language can be expressed as a program in a declarative language. Not only does this render the semantics executable, but it opens up the possibility of applying to imperative languages such as Java or C the advances made in program analysis and transformation of declarative languages. However the direct application of this approach returns the results of analysis and transformation in the language of the semantics. The problem is to provide a systematic way to relate the results back to the original imperative program. In this paper a method is proposed for carrying out partial evaluation of imperative programs, using a partial evaluator for a declarative language, but returning the results in the syntax of the imperative program which is to be partially evaluated. The approach uses folding to reconstruct a specialised imperative program from a partially evaluated semantics-based interpreter. 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). The tools required are a partial evaluator and a folding mechanism for the declarative language. The correctness of the partial evaluator for the imperative language follows from the correctness of the partial evaluator and folding transformer of the declarative language. Other semantics-based program manipulations are suggested for imperative languages, based on abstract interpretation tools developed for declarative languages.