The semantics and transformation of imperative programs using horn clauses

The feasibility of using Horn clauses as a means of describing and transforming imperative pro-grams is explored. A logical semantics is derived for a typical imperative language. The style of this semantics permits direct translations between the source language and semantical representations. Given the use of Horn clause logic in logic programming, the semantics is particularly useful since models of computation associated with logic programs can be applied to it. Treating the semantics as a logic program means that, in a program transformation context, the semantic representation is particularly well suited to partial evaluation. To support these ideas, an automatic translation system has been implemented which permits translation between programs written in an imperative language and their logical equivalents. In addition, a partial evaluator has been written which meta-interprets the logical representation of an imperative program to produce a partially evaluated result. Using predicative programming, this result can be translated back into the original source code. Thus the system as a whole performs source-to-source transformations of imperative programs.Science, Faculty ofComputer Science, Department ofGraduat