Analysis and Specialisation of Imperative Programs: An approach using CLP

Program analysis and specialisation for declarative languages have been subjects of active research during the last 2 decades or so. Imperative languages could benefit from the advances made in declarative languages but most research on analysis and specialisation is language-specific. Thus, it would be desirable to build connections between both worlds, enabling the transfer of results from one to the other. 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 (as potentially) executable, but it opens up the possibility of applying to imperative languages the advances made in program analysis and transformation of declarative languages. This thesis presents results on analysis and specialisation of imperative programs through analysis and specialisation of constraint logic programs. The cornerstone of this connection is a constraint logic program capturing the structural operational semantics of the subject imperative language whose programs are to be specialised and analysed. To provide a connection between imperative programs and constraint logic programs an existing specialiser for logic programs is extended and modified. The extension consists of adding constraints to increase the accuracy of the specialiser. The modification of the specialiser enables the systematic reconstruction of a large class of imperative programs from the specialised constraint logic programs. A key advantage of this approach to analysis and specialisation of imperative programs is that the same tools can be applied to programs in different languages, via their semantics. Also, the correctness of the resulting analysers and specialisers comes from correctness of specialisation and analysis in CLP. The tools needed are a specialiser for CLP and the imperative language semantics as a CLP program. Semantics is provided for a programming language resembling Pascal, though other languages could be used too (e.g. Java or JVM). Through experimentation the generality of the method is shown.