Converting an imperative program to a declarative one

The main issue of this paper is to study the problem of formal translation of programs from an imperative language to a declarative one. To that end, we define a simple imperative language, denoted by L1L1, that supports the basic types of statements that can be found in imperative paradigm such as assignment, looping, and selection or conditional branching. We also define a declarative language, denoted by L2L2, where a program is a set of independent variable definitions that may involve some special arithmetic expressions (conditional expression or recursive expression). For instance, x=5+if(a<3,2∗a,a−1)x=5+if(a<3,2∗a,a−1) could be a definition in L2L2 that affects to x the value 5+2*a if a<3 and otherwise it affects the value 5+(a  −1). The semantics attached to each language is denotational, where the meaning of a program in a given environment (memory state) is an environment. Finally, we introduce a formal translation function that migrates any program in L1L1 to an equivalent (with respect to the semantics) one in L2L2 and we prove its correctness (the semantics of the original version of any program is equal to the semantics of its translated version).