Converting an imperative program to a declarative one

Mohamed Mbarki

doi:10.1016/j.knosys.2005.10.003

Return

Converting an imperative program to a declarative one

2006-06-01

PRE

Mohamed Mbarki *

Mohamed Mejri

Béchir Ktari

DOI：10.1016/j.knosys.2005.10.003

Original

Original request for help

Save

Abstract

En 中文

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 L-1, 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 L-2, 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) could be a definition in L-2 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 L-1 to an equivalent (with respect to the semantics) one in L-2 and we prove its correctness (the semantics of the original version of any program is equal to the semantics of its translated version). (c) 2005 Published by Elsevier B.V.

Keywords:

imperative language

declarative language

denotational semantics

transaltion

AI Summary

Key information extracted from the uploaded paper, including a brief overview, abstract, background, key highlights, visual analysis, and future outlook.