On Transforming Functions Accessing Global Variables into Logically Constrained Term Rewriting Systems

TL;DR

This paper introduces a novel method to transform imperative programs with global variables into logically constrained term rewriting systems, accurately modeling execution environments and function calls.

Contribution

It presents a new transformation approach that encodes global variables and call stacks into term rewriting systems, with proven correctness.

Findings

Accurate modeling of program execution environments.

Transformation preserves program semantics.

Formal proof of transformation correctness.

Abstract

In this paper, we show a new approach to transformations of an imperative program with function calls and global variables into a logically constrained term rewriting system. The resulting system represents transitions of the whole execution environment with a call stack. More precisely, we prepare a function symbol for the whole environment, which stores values for global variables and a call stack as its arguments. For a function call, we prepare rewrite rules to push the frame to the stack and to pop it after the execution. Any running frame is located at the top of the stack, and statements accessing global variables are represented by rewrite rules for the environment symbol. We show a precise transformation based on the approach and prove its correctness.

Equations

$$(3,0,0)\to (3,0,1)\to (3,1,1)\to (3,1,3)\to (3,2,3)\to (3,2,6)\to (3,3,6)\to (3,3,6)$$

$$\mathcal{R}_{1}=\left\{\begin{array}[]{r@{\>}c@{\>}lr@{\,}c@{\,}l}\mathsf{sum1}(x)&\to&\mathsf{u_{1}}(x,\mathsf{0},\mathsf{0}),\\ \mathsf{u_{1}}(x,i,z)&\to&\mathsf{u_{1}}(x,i+\mathsf{1},z+i+\mathsf{1})&\ [&i<x&\,],\\ \mathsf{u_{1}}(x,i,z)&\to&\mathsf{return}(z)&\ [&\neg(i<x)&\,]\\ \end{array}\right\}$$

$$\{\mathsf{g}(x)\to {\mathsf{u}}_2(x,0),{\mathsf{u}}_2(x,z)\to {\mathsf{u}}_3(x,z,sum1(x)),{\mathsf{u}}_3(x,z,\mathsf{return}(y))\to {\mathsf{u}}_4(x,y),{\mathsf{u}}_4(x,z)\to \mathsf{return}(x\times z)\}$$

$$\mathcal{R}_{2}=\left\{\begin{array}[]{r@{\>}c@{\>}lr@{\,}c@{\,}l}\mathsf{sum1}(x,\mathit{num})&\to&\mathsf{u_{1}}(x,\mathsf{0},\mathsf{0},\mathit{num}+\mathsf{1}),\\ \mathsf{u_{1}}(x,i,z,\mathit{num})&\to&\mathsf{u_{1}}(x,i+\mathsf{1},z+i+\mathsf{1},\mathit{num})&\ [&i<x&\,],\\ \mathsf{u_{1}}(x,i,z,\mathit{num})&\to&\mathsf{return}(z,\mathit{num})&\ [&\neg(i<x)&\,],\\[5.0pt] \mathsf{g}(x,\mathit{num})&\to&\mathsf{u_{2}}(x,\mathit{num},\mathsf{0}),\\ \mathsf{u_{2}}(x,\mathit{num},z)&\to&\mathsf{u_{2}^{\prime}}(x,\mathit{num}+\mathsf{1},z),\\ \mathsf{u_{2}^{\prime}}(x,\mathit{num},z)&\to&\mathsf{u_{3}}(x,\mathit{num},z,\mathsf{sum1}(x,\mathit{num})),\\ \mathsf{u_{3}}(x,\mathit{num_{\_}{old}},z,\mathsf{return}(y,\mathit{num_{\_}{new}}))&\to&\mathsf{u_{4}}(x,\mathit{num_{\_}{new}},y),\\ \mathsf{u_{4}}(x,\mathit{num},z)&\to&\mathsf{return}(x\times z,\mathit{num})\\ \end{array}\right\}$$

$$P$$

$$D$$

$$F$$

$$S$$

$$E$$

$$B$$

$$\mathcal{R}_{3}=\left\{\begin{array}[]{r@{\>}c@{\>}lr@{\,}c@{\,}l}\mathsf{sum}(x,\mathit{num})&\to&\mathsf{u_{1}}(x,\mathit{num},\mathsf{0}),\\ \mathsf{u_{1}}(x,\mathit{num},z)&\to&\mathsf{u_{2}}(x,\mathit{num}+\mathsf{1},z),\\ \mathsf{u_{2}}(x,\mathit{num},z)&\to&\mathsf{u_{3}}(x,\mathit{num},z)&\ [&x\leq\mathsf{0}&\,],\\ \mathsf{u_{2}}(x,\mathit{num},z)&\to&\mathsf{u_{5}}(x,\mathit{num},z)&\ [&\neg(x\leq\mathsf{0})&\,],\\ \mathsf{u_{3}}(x,\mathit{num},z)&\to&\mathsf{u_{4}}(x,\mathit{num},\mathsf{0}),\\ \mathsf{u_{4}}(x,\mathit{num},z)&\to&\mathsf{u_{9}}(x,\mathit{num},z),\\ \mathsf{u_{5}}(x,\mathit{num},z)&\to&\mathsf{u_{6}}(x,\mathit{num},z,\mathsf{sum}(x-\mathsf{1})),\\ \mathsf{u_{6}}(x,\mathit{num_{\_}{old}},z,\mathsf{return}(y,\mathit{num_{\_}{new}}))&\to&\mathsf{u_{7}}(x,\mathit{num_{\_}{new}},y),\\ \mathsf{u_{7}}(x,\mathit{num},z)&\to&\mathsf{u_{8}}(x,\mathit{num},x+z),\\ \mathsf{u_{8}}(x,\mathit{num},z)&\to&\mathsf{u_{9}}(x,\mathit{num},z),\\ \mathsf{u_{9}}(x,\mathit{num},z)&\to&\mathsf{return}(z,\mathit{num}),\\[5.0pt] \mathsf{main}(\mathit{num})&\to&\mathsf{u_{10}}(\mathit{num},\mathsf{3}),\\ \mathsf{u_{10}}(\mathit{num},z)&\to&\mathsf{u_{11}}(\mathit{num},z,\mathsf{sum}(z,\mathit{num})),\\ \mathsf{u_{11}}(\mathit{num_{\_}{old}},z,\mathsf{return}(y,\mathit{num_{\_}{new}}))&\to&\mathsf{u_{12}}(y,\mathit{num_{\_}{new}}),\\ \mathsf{u_{12}}(\mathit{num},z)&\to&\mathsf{return}(\mathsf{0},\mathit{num})\\ \end{array}\right\}$$

$$\begin{array}[]{@{}l@{\>}l@{}}\mathsf{main}(\mathsf{0})&\to_{\_}{\mathcal{R}_{3}}\mathsf{u_{10}}(\mathsf{0},\mathsf{3})\\ &\to_{\_}{\mathcal{R}_{3}}\mathsf{u_{11}}(\mathsf{0},\mathsf{3},\mathsf{sum}(\mathsf{3},\mathsf{0}))\\ &\to_{\_}{\mathcal{R}_{3}}\mathsf{u_{11}}(\mathsf{0},\mathsf{3},\mathsf{u_{1}}(\mathsf{3},\mathsf{0},\mathsf{0}))\\ &\to_{\_}{\mathcal{R}_{3}}\mathsf{u_{11}}(\mathsf{0},\mathsf{3},\mathsf{u_{2}}(\mathsf{3},\mathsf{0}+\mathsf{1}))\\ &\to_{\_}{\mathcal{R}_{3}}\mathsf{u_{11}}(\mathsf{0},\mathsf{3},\mathsf{u_{2}}(\mathsf{3},\mathsf{1},\mathsf{0}))\\ &\to_{\_}{\mathcal{R}_{3}}\mathsf{u_{11}}(\mathsf{0},\mathsf{3},\mathsf{u_{5}}(\mathsf{3},\mathsf{1},\mathsf{0}))\\ &\to_{\_}{\mathcal{R}_{3}}\mathsf{u_{11}}(\mathsf{0},\mathsf{3},\mathsf{u_{6}}(\mathsf{3},\mathsf{1},\mathsf{0},\mathsf{sum}(\mathsf{3}-\mathsf{1},\mathsf{1})))\\ &\to_{\_}{\mathcal{R}_{3}}\mathsf{u_{11}}(\mathsf{0},\mathsf{3},\mathsf{u_{6}}(\mathsf{3},\mathsf{1},\mathsf{0},\mathsf{sum}(\mathsf{2},\mathsf{1})))\\ &\to_{\_}{\mathcal{R}_{3}}\cdots\\ &\to_{\_}{\mathcal{R}_{3}}\mathsf{u_{11}}(\mathsf{0},\mathsf{3},\mathsf{u_{7}}(\mathsf{3},\mathsf{4},\mathsf{3})))\\ &\to_{\_}{\mathcal{R}_{3}}\mathsf{u_{11}}(\mathsf{0},\mathsf{3},\mathsf{u_{8}}(\mathsf{3},\mathsf{4},\mathsf{3}+\mathsf{3})))\\ &\to_{\_}{\mathcal{R}_{3}}\mathsf{u_{11}}(\mathsf{0},\mathsf{3},\mathsf{u_{8}}(\mathsf{3},\mathsf{4},\mathsf{6})))\\ &\to_{\_}{\mathcal{R}_{3}}\mathsf{u_{11}}(\mathsf{0},\mathsf{3},\mathsf{u_{9}}(\mathsf{3},\mathsf{4},\mathsf{6}))\\ &\to_{\_}{\mathcal{R}_{3}}\mathsf{u_{11}}(\mathsf{0},\mathsf{3},\mathsf{return}(\mathsf{6},\mathsf{4}))\\ &\to_{\_}{\mathcal{R}_{3}}\mathsf{u_{12}}(\mathsf{6},\mathsf{4})\\ &\to_{\_}{\mathcal{R}_{3}}\mathsf{return}(\mathsf{0},\mathsf{4})\\ \end{array}$$

$$\mathsf{env}(0,\mathsf{main}())$$

$$\left\{\begin{array}[]{r@{\>}c@{\>}lr@{\,}c@{\,}l}\mathsf{main}()&\to&\mathsf{u_{10}}(\mathsf{3}),\\ \mathsf{u_{10}}(z)&\to&\mathsf{u_{11}}(z,\mathsf{sum}(z)),\\ \mathsf{u_{11}}(z,\mathsf{return}(y))&\to&\mathsf{u_{11}}(y),\\ \mathsf{u_{12}}(z)&\to&\mathsf{return}(\mathsf{0}),\\[5.0pt] \mathsf{sum}(x)&\to&\mathsf{u_{1}}(x,\mathsf{0})\\ \end{array}\right\}$$

$$\mathsf{env}(num,{\mathsf{u}}_{11}(z_{\_}0,{\mathsf{u}}_1(x,z)))\to \mathsf{env}(num+1,{\mathsf{u}}_{11}(z_{\_}0,{\mathsf{u}}_2(x,z)))$$

$$\left\{\begin{array}[]{r@{\>}c@{\>}lr@{\,}c@{\,}l}\mathsf{u_{2}}(x,z)&\to&\mathsf{u_{3}}(x,z)&\ [&x\leq\mathsf{0}&\,],\\ \mathsf{u_{2}}(x,z)&\to&\mathsf{u_{5}}(x,z)&\ [&\neg(x\leq\mathsf{0})&\,],\\ \mathsf{u_{3}}(x,z)&\to&\mathsf{u_{4}}(x,\mathsf{0}),\\ \mathsf{u_{4}}(x,z)&\to&\mathsf{u_{9}}(x,z),\\ \mathsf{u_{5}}(x,z)&\to&\mathsf{u_{6}}(x,z,\mathsf{sum}(x-\mathsf{1})),\\ \mathsf{u_{6}}(x,z,\mathsf{return}(y))&\to&\mathsf{u_{7}}(x,y),\\ \mathsf{u_{7}}(x,z)&\to&\mathsf{u_{8}}(x,x+z),\\ \mathsf{u_{8}}(x,z)&\to&\mathsf{u_{9}}(x,z),\\ \mathsf{u_{9}}(x,z)&\to&\mathsf{return}(z)\\ \end{array}\right\}$$

$$\mathsf{env}(num,{\mathsf{u}}_{11}(z_{\_}0,{\mathsf{u}}_6(x^{\prime },z^{\prime },{\mathsf{u}}_1(x,z))))\to \mathsf{env}(num+1,{\mathsf{u}}_{11}(z_{\_}0,{\mathsf{u}}_6(x^{\prime },z^{\prime },{\mathsf{u}}_2(x,z))))$$

$$\mathsf{env}(num,{\mathsf{u}}_{11}(z_{\_}0,{\mathsf{u}}_6(x^{\prime },z^{\prime },{\mathsf{u}}_6(x^{\prime \prime },z^{\prime \prime },{\mathsf{u}}_1(x,z)))))\to \mathsf{env}(num+1,{\mathsf{u}}_{11}(z_{\_}0,{\mathsf{u}}_6(x^{\prime },z^{\prime },{\mathsf{u}}_6(x^{\prime \prime },z^{\prime \prime },{\mathsf{u}}_2(x,z)))))$$

$$\mathsf{env}(0,\mathsf{stack}(\mathsf{main}(),\perp ))$$

$$\left\{\begin{array}[]{r@{\>}c@{\>}l}\mathsf{stack}(\mathsf{u_{5}}(x,z),s)&\to&\mathsf{stack}(\mathsf{sum}(x-\mathsf{1}),\mathsf{stack}(\mathsf{u_{6}}(x,z),s)),\\ \mathsf{stack}(\mathsf{return}(y),\mathsf{stack}(\mathsf{u_{6}}(x,z),s))&\to&\mathsf{stack}(\mathsf{u_{7}}(x,y),s),\\[5.0pt] \mathsf{stack}(\mathsf{u_{10}}(n),s)&\to&\mathsf{stack}(\mathsf{sum}(n),\mathsf{stack}(\mathsf{u_{11}}(n),s)),\\ \mathsf{stack}(\mathsf{return}(y),\mathsf{stack}(\mathsf{u_{11}}(n)))&\to&\mathsf{stack}(\mathsf{u_{3}}(n),s)\\ \end{array}\right\}$$

$$\mathsf{env}(x_{\_}1,\dots ,x_{\_}k,\mathsf{stack}(\mathsf{f}(\dots ),s))\to \mathsf{env}(t_{\_}1,\dots ,t_{\_}k,\mathsf{stack}(\mathsf{g}(\dots ),s))[\phi ]$$

$$\mathsf{env}(num,\mathsf{stack}({\mathsf{u}}_1(x,z),s))\to \mathsf{env}(num+1,\mathsf{stack}({\mathsf{u}}_2(x,z),s))$$

$$\mathcal{R}_{4}=\left\{\begin{array}[]{r@{\>}c@{\>}lr@{\,}c@{\,}l}\mathsf{sum}(x)&\to&\mathsf{u_{1}}(x,\mathsf{0}),\\ \mathsf{env}(\mathit{num},\mathsf{stack}(\mathsf{u_{1}}(x,z),s))&\to&\mathsf{env}(\mathit{num}+\mathsf{1},\mathsf{stack}(\mathsf{u_{2}}(x,z),s)),\\ \mathsf{u_{2}}(x,z)&\to&\mathsf{u_{3}}(x,z)&\ [&x\leq\mathsf{0}&\,],\\ \mathsf{u_{2}}(x,z)&\to&\mathsf{u_{5}}(x,z)&\ [&\neg(x\leq\mathsf{0})&\,],\\ \mathsf{u_{3}}(x,z)&\to&\mathsf{u_{4}}(x,\mathsf{0}),\\ \mathsf{u_{4}}(x,z)&\to&\mathsf{u_{9}}(x,z),\\ \mathsf{stack}(\mathsf{u_{5}}(x,z),s)&\to&\mathsf{stack}(\mathsf{sum}(x-\mathsf{1}),\mathsf{stack}(\mathsf{u_{6}}(x,z),s)),\\ \mathsf{stack}(\mathsf{return}(y),\mathsf{stack}(\mathsf{u_{6}}(x,z),s))&\to&\mathsf{stack}(\mathsf{u_{7}}(x,y),s),\\ \mathsf{u_{7}}(x,z)&\to&\mathsf{u_{8}}(x,x+z),\\ \mathsf{u_{8}}(x,z)&\to&\mathsf{u_{9}}(x,z),\\ \mathsf{u_{9}}(x,z)&\to&\mathsf{return}(z),\\[5.0pt] \mathsf{main}()&\to&\mathsf{u_{10}}(\mathsf{3}),\\ \mathsf{stack}(\mathsf{u_{10}}(z),s)&\to&\mathsf{stack}(\mathsf{sum}(z),\mathsf{stack}(\mathsf{u_{11}}(z),s)),\\ \mathsf{stack}(\mathsf{return}(y),\mathsf{stack}(\mathsf{u_{11}}(z)))&\to&\mathsf{stack}(\mathsf{u_{12}}(y),s),\\ \mathsf{u_{12}}(z)&\to&\mathsf{return}(\mathsf{0})\\ \end{array}\right\}$$

$$\begin{array}[]{@{}l@{\>\>\>}l@{}}\mathsf{env}(\mathsf{0},\mathsf{stack}(\mathsf{main}(),\bot))&\to_{\_}{\mathcal{R}_{4}}\mathsf{env}(\mathsf{0},\mathsf{stack}(\mathsf{u_{10}}(\mathsf{3}),\bot))\\ &\to_{\_}{\mathcal{R}_{4}}\mathsf{env}(\mathsf{0},\mathsf{stack}(\mathsf{sum}(\mathsf{3}),\mathsf{stack}(\mathsf{u_{11}}(\mathsf{3}),\bot)))\\ &\to_{\_}{\mathcal{R}_{4}}\mathsf{env}(\mathsf{0},\mathsf{stack}(\mathsf{u_{1}}(\mathsf{3},\mathsf{0}),\mathsf{stack}(\mathsf{u_{11}}(\mathsf{3}),\bot)))\\ &\to_{\_}{\mathcal{R}_{4}}\mathsf{env}(\mathsf{0}+\mathsf{1},\mathsf{stack}(\mathsf{u_{2}}(\mathsf{3},\mathsf{0}),\mathsf{stack}(\mathsf{u_{11}}(\mathsf{3}),\bot)))\\ &\to_{\_}{\mathcal{R}_{4}}\mathsf{env}(\mathsf{1},\mathsf{stack}(\mathsf{u_{2}}(\mathsf{3},\mathsf{0}),\mathsf{stack}(\mathsf{u_{11}}(\mathsf{3}),\bot)))\\ &\to_{\_}{\mathcal{R}_{4}}\mathsf{env}(\mathsf{1},\mathsf{stack}(\mathsf{u_{5}}(\mathsf{3},\mathsf{0}),\mathsf{stack}(\mathsf{u_{11}}(\mathsf{3}),\bot)))\\ &\to_{\_}{\mathcal{R}_{4}}\mathsf{env}(\mathsf{1},\mathsf{stack}(\mathsf{sum}(\mathsf{3}-\mathsf{1}),\mathsf{stack}(\mathsf{u_{6}}(\mathsf{3},\mathsf{0}),\mathsf{stack}(\mathsf{u_{11}}(\mathsf{3}),\bot))))\\ &\to_{\_}{\mathcal{R}_{4}}\mathsf{env}(\mathsf{1},\mathsf{stack}(\mathsf{sum}(\mathsf{2}),\mathsf{stack}(\mathsf{u_{6}}(\mathsf{3},\mathsf{0}),\mathsf{stack}(\mathsf{u_{11}}(\mathsf{3}),\bot))))\\ &\to_{\_}{\mathcal{R}_{4}}\cdots\\ &\to_{\_}{\mathcal{R}_{4}}\mathsf{env}(\mathsf{4},\mathsf{stack}(\mathsf{u_{7}}(\mathsf{3},\mathsf{3}),\mathsf{stack}(\mathsf{u_{11}}(\mathsf{3}),\bot)))\\ &\to_{\_}{\mathcal{R}_{4}}\mathsf{env}(\mathsf{4},\mathsf{stack}(\mathsf{u_{8}}(\mathsf{3},\mathsf{3}+\mathsf{3}),\mathsf{stack}(\mathsf{u_{11}}(\mathsf{3}),\bot)))\\ &\to_{\_}{\mathcal{R}_{4}}\mathsf{env}(\mathsf{4},\mathsf{stack}(\mathsf{u_{8}}(\mathsf{3},\mathsf{6}),\mathsf{stack}(\mathsf{u_{11}}(\mathsf{3}),\bot)))\\ &\to_{\_}{\mathcal{R}_{4}}\mathsf{env}(\mathsf{4},\mathsf{stack}(\mathsf{u_{9}}(\mathsf{3},\mathsf{6}),\mathsf{stack}(\mathsf{u_{11}}(\mathsf{3}),\bot)))\\ &\to_{\_}{\mathcal{R}_{4}}\mathsf{env}(\mathsf{4},\mathsf{stack}(\mathsf{return}(\mathsf{6}),\mathsf{stack}(\mathsf{u_{11}}(\mathsf{3}),\bot)))\\ &\to_{\_}{\mathcal{R}_{4}}\mathsf{env}(\mathsf{4},\mathsf{stack}(\mathsf{u_{12}}(\mathsf{6},\bot)))\\ &\to_{\_}{\mathcal{R}_{4}}\mathsf{env}(\mathsf{4},\mathsf{stack}(\mathsf{return}(\mathsf{0})))\\ \end{array}$$

$$\begin{array}[]{@{}l@{}}\mathtt{int}~{}x_{\_}1~{}=~{}n_{\_}1;~{}\ldots;~{}\mathtt{int}~{}x_{\_}k~{}=~{}n_{\_}k;\\ \mathtt{int}~{}\mathsf{f}_{\_}1(\mathtt{int}~{}y_{\_}{1,1},\ldots,\mathtt{int}~{}y_{\_}{1,m_{\_}1})~{}\{~{}\alpha_{\_}1~{}~{}\mathtt{return}~{}e_{\_}1;~{}\}\\ ~{}~{}~{}~{}~{}\ldots\\ \mathtt{int}~{}\mathsf{f}_{\_}{k^{\prime}}(\mathtt{int}~{}y_{\_}{k^{\prime},1},\ldots,\mathtt{int}~{}y_{\_}{k^{\prime},m_{\_}{k^{\prime}}})~{}\{~{}\alpha_{\_}{k^{\prime}}~{}~{}\mathtt{return}~{}e_{\_}{k^{\prime}};~{}\}\\ \end{array}$$

$$(u,\!\left\{\begin{array}[]{@{}r@{\,}c@{\,}l@{\!}}C[\mathsf{stack}(g(\overrightarrow{y},\overrightarrow{z}),w)]&\to&C[\mathsf{stack}(\mathsf{f}_{\_}{k^{\prime\prime}}(\overrightarrow{e^{\prime}_{k^{\prime\prime}}}),\mathsf{stack}(\mathsf{u}_{\_}i(\overrightarrow{y},\overrightarrow{z}),w))],\\ C^{\prime}[\mathsf{stack}(\mathsf{return}(z^{\prime\prime}),\mathsf{stack}(\mathsf{u}_{\_}i(\overrightarrow{y},\overrightarrow{z}),w))]&\to&(C^{\prime}[\mathsf{stack}(\mathsf{u}_{\_}{i+1}(\overrightarrow{y},\overrightarrow{z}),w)])\{z^{\prime}\mapsto z^{\prime\prime}\}\\ \end{array}\right\}\!\cup\mathcal{R}_{\_}\beta,j)$$

$$(u,\left\{\begin{array}[]{r@{\>}c@{\>}l@{~~}c@{\,}c@{\,}c@{~~~~~~}r@{\>}c@{\>}l}C[g(\overrightarrow{y},\overrightarrow{z})]&\to&C[\mathsf{u}_{\_}i(\overrightarrow{y},\overrightarrow{z})]\hfil~{}~{}&\ [&\varphi&\,],\hfil~{}~{}~{}~{}~{}~{}&u_{\_}1&\to&\mathsf{u}_{\_}{j_{\_}2}(\overrightarrow{y},\overrightarrow{z}),\\ C[g(\overrightarrow{y},\overrightarrow{z})]&\to&C[\mathsf{u}_{\_}{j_{\_}1+1}(\overrightarrow{y},\overrightarrow{z})]\hfil~{}~{}&\ [&\neg\varphi&\,],\hfil~{}~{}~{}~{}~{}~{}&u_{\_}2&\to&\mathsf{u}_{\_}{j_{\_}2}(\overrightarrow{y},\overrightarrow{z})\\ \end{array}\right\}\cup\mathcal{R}_{\_}{\beta_{\_}1}\cup\mathcal{R}_{\_}{\beta_{\_}2}\cup\mathcal{R}_{\_}\beta,j)$$

$$(u^{\prime},\left\{\begin{array}[]{r@{\>}c@{\>}l@{~~}c@{\,}c@{\,}c@{~~~~~~}r@{\>}c@{\>}l}C[g(\overrightarrow{y},\overrightarrow{z})]&\to&C[\mathsf{u}_{\_}i(\overrightarrow{y},\overrightarrow{z})]\hfil~{}~{}&\ [&\varphi&\,],\hfil~{}~{}~{}~{}~{}~{}&u&\to&g(\overrightarrow{y},\overrightarrow{z}),\\ C[g(\overrightarrow{y},\overrightarrow{z})]&\to&C[\mathsf{u}_{\_}j(\overrightarrow{y},\overrightarrow{z})]\hfil~{}~{}&\ [&\neg\varphi&\,]\hfil~{}~{}~{}~{}~{}~{}\\ \end{array}\right\}\cup\mathcal{R}_{\_}\alpha\cup\mathcal{R}_{\_}\beta,j^{\prime})$$

$$(\mathsf{env}(\vec{x},\mathsf{stack}(g(\overrightarrow{y},\overrightarrow{z}),s))({\sigma }_{\_}0\cup {\sigma }_{\_}1){\to }_{\_}^{\ast }\mathcal{R}(\mathsf{env}(\vec{x},\mathsf{stack}(u,s)))({\sigma }_{\_}{0}^{\prime }\cup {\sigma }_{\_}{1}^{\prime }).$$

$$(u,\!\left\{\begin{array}[]{@{}r@{\,}c@{\,}l@{}}C^{\prime}[\mathsf{stack}(g(\overrightarrow{y},\overrightarrow{z}),w)]&\to&C^{\prime}[\mathsf{stack}(\mathsf{f}_{\_}{k^{\prime\prime}}(\overrightarrow{e^{\prime}_{k^{\prime\prime}}}),\mathsf{stack}(\mathsf{u}_{\_}{i^{\prime}}(\overrightarrow{y},\overrightarrow{z}),w))],\\ C^{\prime\prime}[\mathsf{stack}(\mathsf{return}(z^{\prime\prime}),\mathsf{stack}(\mathsf{u}_{\_}{i^{\prime}}(\overrightarrow{y},\overrightarrow{z}),w))]&\to&(C^{\prime\prime}[\mathsf{stack}(\mathsf{u}_{\_}{i^{\prime}+1}(\overrightarrow{y},\overrightarrow{z}),w)])\{z^{\prime}\mapsto z^{\prime\prime}\}\\ \end{array}\right\}\!\cup\mathcal{R}_{\_}{\beta^{\prime}},j)$$

$$\begin{array}[]{@{}l@{\>}c@{\>}l@{}}\lx@intercol\@ADDCLASS{ltx_eqn_lefteqn}$\displaystyle(\mathsf{env}(\vec{x},\mathsf{stack}(g(\overrightarrow{y},\overrightarrow{z}),s)))(\sigma_{\_}0\cup\sigma_{\_}1)$\mbox{}\hfil\lx@intercol\\ {}{}{}{}&\mathrel{\to_{\_}\mathcal{R}}&(\mathsf{env}(\vec{x},\mathsf{stack}(\mathsf{f}_{\_}{k^{\prime\prime}}(\overrightarrow{e^{\prime}_{k^{\prime\prime}}}),\mathsf{stack}(\mathsf{u}_{\_}{i^{\prime}}(\overrightarrow{y},\overrightarrow{z}),s))))(\sigma_{\_}0\cup\sigma_{\_}1)\\ &=&(\mathsf{env}((\vec{x})\sigma_{\_}0,\mathsf{stack}(\mathsf{f}_{\_}{k^{\prime\prime}}((\overrightarrow{e^{\prime}_{k^{\prime\prime}}})(\sigma_{\_}0\cup\sigma_{\_}1)),\mathsf{stack}(\mathsf{u}_{\_}{i^{\prime}}((\overrightarrow{y})\sigma_{\_}1,(\overrightarrow{z})\sigma_{\_}1),s))))\\ &\mathrel{\to^{*}_{\_}\mathcal{R}}&(\mathsf{env}((\vec{x})\sigma_{\_}0,\mathsf{stack}(\mathsf{f}_{\_}{k^{\prime\prime}}(n_{\_}1,\ldots,n_{\_}{m_{\_}{k^{\prime\prime}}}),\mathsf{stack}(\mathsf{u}_{\_}{i^{\prime}}((\overrightarrow{y})\sigma_{\_}1,(\overrightarrow{z})\sigma_{\_}1),s)))).\\ \end{array}$$

$$(\mathsf{env}(\vec{x},\mathsf{stack}({\mathsf{f}}_{\_}{k}^{\prime \prime }(\overrightarrow{y_{k^{\prime \prime }}}),s^{\prime }))({\sigma }_{\_}0\cup {\sigma }_{\_}2){\to }_{\_}^{\ast }\mathcal{R}(\mathsf{env}(\vec{x},\mathsf{stack}(u_{\_}{k}^{\prime \prime },s^{\prime }))({\sigma }_{\_}{0}^{\prime \prime }\cup {\sigma }_{\_}{1}^{\prime \prime }).$$

$$\begin{array}[]{@{}l@{\>}c@{\>}l@{}}\lx@intercol\@ADDCLASS{ltx_eqn_lefteqn}$\displaystyle(\mathsf{env}((\vec{x})\sigma_{\_}0,\mathsf{stack}(\mathsf{f}_{\_}{k^{\prime\prime}}(n_{\_}1,\ldots,n_{\_}{m_{\_}{k^{\prime\prime}}}),\mathsf{stack}(\mathsf{u}_{\_}{i^{\prime}}((\overrightarrow{y})\sigma_{\_}1,(\overrightarrow{z})\sigma_{\_}1),s))))$\mbox{}\hfil\lx@intercol\\ {}{}{}{}&=&\mathsf{env}((\vec{x})\sigma_{\_}0,\mathsf{stack}(\mathsf{f}_{\_}{k^{\prime\prime}}((\overrightarrow{y_{k^{\prime\prime}}})\sigma_{\_}2),\mathsf{stack}(\mathsf{u}_{\_}{i^{\prime}}((\overrightarrow{y})\sigma_{\_}1,(\overrightarrow{z})\sigma_{\_}1),s))))\\ &\mathrel{\to^{*}_{\_}\mathcal{R}}&\mathsf{env}((\vec{x})\sigma_{\_}0^{\prime\prime},\mathsf{stack}(u_{\_}{k^{\prime\prime}}(\sigma_{\_}0^{\prime\prime}\cup\sigma_{\_}1^{\prime\prime}),\mathsf{stack}(\mathsf{u}_{\_}{i^{\prime}}((\overrightarrow{y})\sigma_{\_}1,(\overrightarrow{z})\sigma_{\_}1),s)))).\\ \end{array}$$

Full text

1 Introduction

Recently, analyses of imperative programs (written in C, Java Bytecode, etc.) via transformations into term rewriting systems have been investigated [3, 4, 7, 12]. In particular, constrained rewriting systems are popular for these transformations, since logical constraints used for modeling the control flow can be separated from terms expressing intermediate states [3, 4, 7, 10, 14]. To capture the existing approaches for constrained rewriting in one setting, the framework of a logically constrained term rewriting system (an LCTRS, for short) has been proposed [8]. Transformations of C programs with integers, characters, arrays of integers, global variables, and so on into LCTRSs have been discussed in [6].

A basic idea of transforming functions defined in simple imperative programs over the integers, so-called while programs, is to represent transitions of parameters and local variables as rewrite rules with auxiliary function symbols. The resulting rewriting system can be considered a transition system w.r.t. parameters and local variables. Consider the function $\mathtt{sum1}$ in Figure 1, which is written in the C language. The function sum1 computes the summation from [math] to a given non-negative integer $x$. The execution of the body of this function can be considered a transition of values for $x$, $i$, and $z$, respectively. For example, we have the following transition for sum1(3):

[TABLE]

This transition for the execution of the function $\mathtt{sum1}$ can be modeled by an LCTRS as follows [7, 6]:

[TABLE]

Note that the auxiliary function symbol $\mathsf{u_{1}}$ can be considered locations stored in the program counter. The transformed LCTRS is useful to verify the original program [6]. For example, the theorem proving method based on rewriting induction [13] can automatically prove that $\forall n\in\mathbb{Z}.\ \mathsf{sum1}(n)=\frac{n(n+1)}{2}$, i.e., correctness of the C program [14, 9, 6].

A function call is added as an extra argument of the auxiliary symbol that corresponds to the statement of the call. Let us consider the following function in addition to $\mathtt{sum1}$ in Figure 1:

int g(int x){
  int z = 0;
  z = sum1(x);
  return x * z;
}

This function is transformed into the following rules:

[TABLE]

The auxiliary function symbol $\mathsf{u_{2}}$ calls $\mathsf{sum1}$ in the third argument of $\mathsf{u_{3}}$ by means of the rule for $\mathsf{u_{2}}$.

To deal with a global variable under sequential execution, it is enough to pass a value stored in the global variable to a function call as an extra argument and to receive from the called function a value of the global variable that may be updated in executing the function call, restoring the value in the global variable. Let us add a global variable counting the total number of function calls to the above program as in Figure 2. This program is transformed into the following LCTRS [6]:

[TABLE]

The above approach to transformations of function calls is very naive but not general. For example, to model parallel execution, a value stored in a global variable does not have to be passed to a particular function or a process because another function or process may access the global variable.

In this paper, we show another approach to transformations of imperative programs with function calls and global variables into LCTRSs. Our target languages are call-by-value imperative languages such as C. For this reason, we use a small subclass of C programs over the integers as fundamental imperative programs. We show a precise transformation along the approach and prove its correctness.

Our idea of the treatment for global variables in calling functions is to prepare a new symbol to represent the whole environment for execution. Values of global variables are stored in arguments of the new symbol, and transitions accessing global variables are represented as transitions of the environment. In reduction sequences of LCTRSs obtained by the original transformation, positions of function calls are not unique, and thus, we may need (possibly infinitely) many rules for a transition related to a global variable. To solve this problem, we prepare a so-called call stack, and transform programs into LCTRSs that specify statements as rewrite rules for not only user-defined functions but also the introduced symbol of the environment. In calling a function, a frame of the called function is pushed to the stack, and popped from the stack when the execution halts successfully. This implies that any running frame is located at the top of the stack, i.e., positions of function calls are unique. We transform statements not accessing global variables into rewrite rules for called functions as well as the previous transformation, and transform statements accessing global variables into rewrite rules for the introduced symbol for the environment.

This paper is organized as follows. In Section 2, we recall LCTRSs and a small imperative language. In Section 3, using an example, we show a new approach to transformations of imperative programs into LCTRSs. In Section 4, we precisely define a transformation and show its correctness. In Section 5, we describe a future direction of this research.

2 Preliminaries

In this section, we recall LCTRSs, following the definitions in [8, 6]. We also recall a small imperative language SIMP+ with global variables and function calls. Familiarity with basic notions on term rewriting [2, 11] is assumed.

2.1 Logically Constrained Term Rewriting Systems

Let $\mathcal{S}$ be a set of sorts and $\mathcal{V}$ a countably infinite set of variables, each of which is equipped with a sort. A signature $\Sigma$ is a set, disjoint from $\mathcal{V}$, of function symbols $f$, each of which is equipped with a sort declaration $\iota_{\_}1\times\cdots\times\iota_{\_}n\Rightarrow\iota$ where $\iota_{\_}1,\ldots,\iota_{\_}n,\iota\in\mathcal{S}$. For readability, we often write $\iota$ instead of $\iota_{\_}1\times\cdots\times\iota_{\_}n\Rightarrow\iota$ if $n=0$. We denote the set of well-sorted terms over $\Sigma$ and $\mathcal{V}$ by $T(\Sigma,\mathcal{V})$. In the rest of this section, we fix $\mathcal{S}$, $\Sigma$, and $\mathcal{V}$. The set of variables occurring in $s_{\_}1,\ldots,s_{\_}n$ is denoted by ${\mathcal{V}\mathit{ar}}(s_{\_}1,\ldots,s_{\_}n)$. Given a term $s$ and a position $p$ (a sequence of positive integers) of $s$, $s|_{\_}p$ denotes the subterm of $s$ at position $p$, and $s[t]_{\_}p$ denotes $s$ with the subterm at position $p$ replaced by $t$. A context $C[~{}]$ is a term containing one hole $\Box_{\_}\iota:\iota$. For a term $s:\iota$, $C[s]$ denotes the term obtained from $C[\,]$ by replacing $\Box_{\_}\iota$ by $s$.

A substitution $\gamma$ is a sort-preserving total mapping from $\mathcal{V}$ to $T(\Sigma,\mathcal{V})$, and naturally extended for a mapping from $T(\Sigma,\mathcal{V})$ to $T(\Sigma,\mathcal{V})$: the result $s\gamma$ of applying a substitution $\gamma$ to a term $s$ is $s$ with all occurrences of a variable $x$ replaced by $\gamma(x)$. The domain ${\mathcal{D}\mathit{om}}(\gamma)$ of $\gamma$ is the set of variables $x$ with $\gamma(x)\neq x$. The notation $\{x_{\_}1\mapsto s_{\_}1,\ldots,x_{\_}k\mapsto s_{\_}k\}$ denotes a substitution $\gamma$ with $\gamma(x_{\_}i)=s_{\_}i$ for $1\leq i\leq n$, and $\gamma(y)=y$ for $y\notin\{x_{\_}1,\ldots,x_{\_}n\}$.

To define LCTRSs, we consider different kinds of symbols and terms: (1) two signatures $\Sigma_{\mathit{terms}}$ and $\Sigma_{\mathit{theory}}$ such that $\Sigma=\Sigma_{\mathit{terms}}\cup\Sigma_{\mathit{theory}}$, (2) a mapping $\mathcal{I}$ which assigns to each sort $\iota$ occurring in $\Sigma_{\mathit{theory}}$ a set $\mathcal{I}_{\_}\iota$, (3) a mapping $\mathcal{J}$ which assigns to each $f:\iota_{\_}1\times\cdots\times\iota_{\_}n\Rightarrow\iota\in\Sigma_{\mathit{theory}}$ a function in $\mathcal{I}_{\_}{\iota_{\_}1}\times\cdots\times\mathcal{I}_{\_}{\iota_{\_}n}\Rightarrow\mathcal{I}_{\_}\iota$, and (4) a set ${\mathcal{V}\mathit{al}}_{\_}\iota\subseteq\Sigma_{\mathit{theory}}$ of values—function symbols $a:\iota$ such that $\mathcal{J}$ gives a bijective mapping from ${\mathcal{V}\mathit{al}}_{\_}\iota$ to $\mathcal{I}_{\_}\iota$—for each sort $\iota$ occurring in $\Sigma_{\mathit{theory}}$. We require that $\Sigma_{\mathit{terms}}\cap\Sigma_{\mathit{theory}}\subseteq{\mathcal{V}\mathit{al}}=\bigcup_{\_}{\iota\in\mathcal{S}}{\mathcal{V}\mathit{al}}_{\_}\iota$. The sorts occurring in $\Sigma_{\mathit{theory}}$ are called theory sorts, and the symbols theory symbols. Symbols in ${\Sigma_{\mathit{theory}}}\setminus{{\mathcal{V}\mathit{al}}}$ are calculation symbols. A term in $T(\Sigma_{\mathit{theory}},\mathcal{V})$ is called a theory term. For ground theory terms, we define the interpretation as $\llbracket f(s_{\_}1,\ldots,s_{\_}n)\rrbracket=\mathcal{J}(f)(\llbracket s_{\_}1\rrbracket,\ldots,\llbracket s_{\_}n\rrbracket)$. For every ground theory term $s$, there is a unique value $c$ such that $\llbracket s\rrbracket=\llbracket c\rrbracket$. We use infix notation for theory and calculation symbols.

A constraint is a theory term $\varphi$ of some sort $\mathit{bool}$ with $\mathcal{I}_{\_}\mathit{bool}=\mathbb{B}=\{\top,\bot\}$, the set of booleans. A constraint $\varphi$ is valid if $\llbracket\varphi\gamma\rrbracket=\top$ for all substitutions $\gamma$ which map ${\mathcal{V}\mathit{ar}}(\varphi)$ to values, and satisfiable if $\llbracket\varphi\gamma\rrbracket=\top$ for some such substitution. A substitution $\gamma$ respects $\varphi$ if $\gamma(x)$ is a value for all $x\in{\mathcal{V}\mathit{ar}}(\varphi)$ and $\llbracket\varphi\gamma\rrbracket=\top$. We typically choose a theory signature with $\Sigma_{\mathit{theory}}\supseteq\Sigma_{\mathit{theory}}^{\mathit{core}}$, where $\Sigma_{\mathit{theory}}^{\mathit{core}}$ contains $\mathsf{true},\mathsf{false}:\mathit{bool}$, $\wedge,\vee,\implies:\mathit{bool}\times\mathit{bool}\Rightarrow\mathit{bool}$, $\neg:\mathit{bool}\Rightarrow\mathit{bool}$, and, for all theory sorts $\iota$, symbols $=_{\_}\iota,\neq_{\_}\iota:\iota\times\iota\Rightarrow\mathit{bool}$, and an evaluation function $\mathcal{J}$ that interprets these symbols as expected. We omit the sort subscripts from $=$ and $\neq$ when they are clear from context.

The standard integer signature $\Sigma_{\mathit{theory}}^{\mathit{int}}$ is $\Sigma_{\mathit{theory}}^{\mathit{core}}\cup\{+,-,*,\mathsf{exp},\mathsf{div},\mathsf{mod}:\mathit{int}\times\mathit{int}\Rightarrow\mathit{int}\}\cup\{{\geq},{>}:\mathit{int}\times\mathit{int}\Rightarrow\mathit{bool}\}\cup\{\mathsf{n}:\mathit{int}\mid n\in\mathbb{Z}\}$ with values $\mathsf{true}$, $\mathsf{false}$, and $\mathsf{n}$ for all integers $n\in\mathbb{Z}$. Thus, we use $\mathsf{n}$ (in sans-serif font) as the function symbol for $n\in\mathbb{Z}$ (in $\mathit{math}$ font). We define $\mathcal{J}$ in the natural way, except: since all $\mathcal{J}(f)$ must be total functions, we set $\mathcal{J}(\mathsf{div})(n,0)=\mathcal{J}(\mathsf{mod})(n,0)=\mathcal{J}(\mathsf{exp})(n,k)=0$ for all $n$ and all $k<0$. When constructing LCTRSs from, e.g., while programs, we can add explicit error checks for, e.g., “division by zero”, to constraints (cf. [6]).

A constrained rewrite rule is a triple $\ell\to r\ [\,\varphi\,]$ such that $\ell$ and $r$ are terms of the same sort, $\varphi$ is a constraint, and $\ell$ has the form $f(\ell_{\_}1,\dots,\ell_{\_}n)$ and contains at least one symbol in $\Sigma_{\mathit{terms}}\setminus\Sigma_{\mathit{theory}}$ (i.e., $\ell$ is not a theory term). If $\varphi=\mathsf{true}$ with $\mathcal{J}(\mathsf{true})=\top$, we may write $\ell\to r$. We define ${\mathcal{LV}\mathit{ar}}(\ell\to r\ [\,\varphi\,])$ as ${\mathcal{V}\mathit{ar}}(\varphi)\cup({\mathcal{V}\mathit{ar}}(r)\setminus{\mathcal{V}\mathit{ar}}(\ell))$. We say that a substitution $\gamma$ respects $\ell\to r\ [\,\varphi\,]$ if $\gamma(x)\in{\mathcal{V}\mathit{al}}$ for all $x\in{\mathcal{LV}\mathit{ar}}(\ell\to r\ [\,\varphi\,])$, and $\llbracket\varphi\gamma\rrbracket=\top$. Note that it is allowed to have ${\mathcal{V}\mathit{ar}}(r)\not\subseteq{\mathcal{V}\mathit{ar}}(\ell)$, but fresh variables in the right-hand side may only be instantiated with values. Given a set $\mathcal{R}$ of constrained rewrite rules, we let $\mathcal{R}_{\mathtt{calc}}$ be the set $\{f(x_{\_}1,\ldots,x_{\_}n)\to y\ [\,y=f(x_{\_}1,\ldots,x_{\_}n)\,]\mid f:\iota_{\_}1\times\cdots\times\iota_{\_}n\Rightarrow\iota\in{\Sigma_{\mathit{theory}}}\setminus{{\mathcal{V}\mathit{al}}}\}$. We usually call the elements of $\mathcal{R}_{\mathtt{calc}}$ constrained rewrite rules (or calculation rules) even though their left-hand side is a theory term. The rewrite relation $\to_{\_}{\mathcal{R}}$ is a binary relation on terms, defined by: $s[\ell\gamma]_{\_}p\mathrel{\to_{\_}\mathcal{R}}s[r\gamma]_{\_}p$ if $\ell\to r\ [\,\varphi\,]\in\mathcal{R}\cup\mathcal{R}_{\mathtt{calc}}$ and $\gamma$ respects $\ell\to r\ [\,\varphi\,]$. We may say that the reduction occurs at position $p$. A reduction step with $\mathcal{R}_{\mathtt{calc}}$ is called a calculation.

Now we define a logically constrained term rewriting system (an LCTRS, for short) as the abstract rewriting system $(T(\Sigma,\mathcal{V}),\to_{\_}\mathcal{R})$ which is simply written by $\mathcal{R}$. An LCTRS is usually given by supplying $\Sigma$, $\mathcal{R}$, and an informal description of $\mathcal{I}$ and $\mathcal{J}$ if these are not clear from context. An LCTRS $\mathcal{R}$ is said to be left-linear if for every rule in $\mathcal{R}$, the left-hand side is linear. $\mathcal{R}$ is said to be non-overlapping if for every term $s$ and rule $\ell\to r\ [\,\varphi\,]$ such that $s$ reduces with $\ell\to r\ [\,\varphi\,]$ at the root position: (a) there are no other rules $\ell^{\prime}\to r^{\prime}\ [\,\varphi^{\prime}\,]$ such that $s$ reduces with $\ell^{\prime}\to r^{\prime}\ [\,\varphi^{\prime}\,]$ at the root position, and (b) if $s$ reduces with any rule at a non-root position $q$, then $q$ is not a position of $\ell$. $\mathcal{R}$ is said to be orthogonal if $\mathcal{R}$ is left-linear and non-overlapping. For $f(\ell_{\_}1,\ldots,\ell_{\_}n)\to r\ [\,\varphi\,]\in\mathcal{R}$, we call $f$ a defined symbol of $\mathcal{R}$, and non-defined elements of $\Sigma_{\mathit{terms}}$ and all values are called constructors of $\mathcal{R}$. Let $\mathcal{D}_{\_}\mathcal{R}$ be the set of all defined symbols and $\mathcal{C}_{\_}\mathcal{R}$ the set of constructors. A term in $T(\mathcal{C}_{\_}\mathcal{R},\mathcal{V})$ is a constructor term of $\mathcal{R}$. We call $\mathcal{R}$ a constructor system if the left-hand side of each rule $\ell\to r\ [\,\varphi\,]\in\mathcal{R}$ is of the form $f(t_{\_}1,\ldots,t_{\_}n)$ with $t_{\_}1,\ldots,t_{\_}n$ constructor terms.

Example 2.1** **([6])

Let $\mathcal{S}=\{\mathit{int},\mathit{bool}\}$, and $\Sigma=\Sigma_{\mathit{terms}}\cup\Sigma_{\mathit{theory}}^{\mathit{int}}$, where $\Sigma_{\mathit{terms}}=\{~{}\mathsf{fact}:\mathit{int}\Rightarrow\mathit{int}~{}\}\cup\{~{}\mathsf{n}:\mathit{int}\mid n\in\mathbb{Z}~{}\}$. Then both $\mathit{int}$ and $\mathit{bool}$ are theory sorts. We also define set and function interpretations, i.e., $\mathcal{I}_{\_}\mathit{int}=\mathbb{Z}$, $\mathcal{I}_{\_}\mathit{bool}=\mathbb{B}$, and $\mathcal{J}$ is defined as above. Examples of theory terms are $\mathsf{0}=\mathsf{0}+\mathsf{-1}$ and $x+\mathsf{3}\geq y+-\mathsf{42}$ that are constraints. $\mathsf{5}+\mathsf{9}$ is also a (ground) theory term, but not a constraint. Using calculation steps, a term $\mathsf{3}-\mathsf{1}$ reduces to $\mathsf{2}$ in one step with the calculation rule $x-y\to z\ [\,z=x-y\,]$, and $\mathsf{3}\times(\mathsf{2}\times(\mathsf{1}\times\mathsf{1}))$ reduces to $\mathsf{6}$ in three steps.

To implement an LCTRS calculating the factorial function, we use the signature $\Sigma$ above and the following rules: $\mathcal{R}_{\_}{\mathsf{fact}}=\{\ \mathsf{fact}(x)\to\mathsf{1}\ [\,x\leq\mathsf{0}\,],~{}~{}\mathsf{fact}(x)\to x\times\mathsf{fact}(x-\mathsf{1})\ [\,\neg(x\leq\mathsf{0})\,]\ \}$. Expected starting terms are, e.g., $\mathsf{fact}(\mathsf{42})$ or $\mathsf{fact}(\mathsf{fact}(\mathsf{-4}))$. Using the constrained rewrite rules in $\mathcal{R}_{\_}{\mathsf{fact}}$, $\mathsf{fact}(\mathsf{3})$ reduces in ten steps to $\mathsf{6}$.

2.2 SIMP+: a Small Imperative Language with Global Variables and Function Calls

In this section, we recall the syntax of SIMP, a small imperative language (cf. [5]). To deal with global variables and function calls, we add them into the ordinary syntax and semantics of SIMP in a natural way. We refer to such an extended language as SIMP+.

We first show the syntax adopting a C-like notation. A program $\mathit{P}$ of SIMP+ is defined by the following BNF:

[TABLE]

where $n\in\mathbb{Z}$, $v\in\mathcal{V}$, $f$ is a function name, and we may omit brackets in the usual way. The empty sequence “$\epsilon$” is used instead of the “skip” command. To simplify discussion, we do not use other operands such as multiplication and division, but we use $\neq$, $\leq$, $>$, $\geq$, $\land$, $\implies$, etc, as syntactic sugars. We also use the for-statement as a syntactic sugar. We assume that a function name $f$ has a fixed arity, and the definition and call of $f$ are consistent with the arity. A program $P$ consists of declarations of global variables (with initialization) and functions. For a program $P$, we denote the set of global variables appearing in $P$ by ${\mathcal{GV}\mathit{ar}}(P)$: let $P$ be $\mathtt{int}~{}x_{\_}1~{}=~{}n_{\_}1;\ldots;\mathtt{int}~{}x_{\_}k~{}=~{}n_{\_}k;\mathtt{int}~{}f(\ldots)~{}=~{}\{\ldots\}~{}\ldots$, then ${\mathcal{GV}\mathit{ar}}(P)=\{x_{\_}1,\ldots,x_{\_}n\}$. We assume that each function $f$ is defined at most once in a program $P$ and any function called in a function defined in $P$ is defined in $P$. To simplify the semantics, we assume that local variables in function declarations are different from global variables and parameters of functions. An assignment is defined by a substitution whose range is over the integers, which may be used for terms in the setting of LCTRSs. We deal with SIMP+ programs that can be successfully compiled as C programs.

Example 2.2

The program $P_{1}$ in Figure 3 is a SIMP+ program, and we have that ${\mathcal{GV}\mathit{ar}}(P_{1})=\{\mathit{num}\}$.

The semantics $\Downarrow_{\mathrm{calc}}$ of integer and boolean expressions is defined as usual (see Figure 4): given an expression $e$ and an assignment $\sigma$ with ${\mathcal{D}\mathit{om}}(\sigma)\supseteq{\mathcal{V}\mathit{ar}}(e)$, we write $(e,\sigma)\Downarrow_{\mathrm{calc}}v$ where $v$ is the resulting value obtained by evaluating $e$ with $\sigma$. The transition system defining the semantics of a SIMP+ program $P$ is defined by

• •

configurations of the form $\langle\alpha,\,\sigma_{\_}0,\,\sigma_{\_}1\rangle$, where

• –

$\alpha$ is of the form “$\delta~{}\beta$” with variable declarations $\delta$,111 Variable declarations $\delta$ may be the empty sequence. and a statement $\beta$, and

• –

$\sigma_{\_}0,\sigma_{\_}1$ are assignments for global and local variables, respectively, which are represented by partial functions from variables to integers—the update $\sigma[x\mapsto n]$ of an assignment $\sigma$ w.r.t. $x$ for an integer $n$ is defined as follows: if $x=y$ then $\sigma[x\mapsto n](y)=n$, and otherwise, $\sigma[x\mapsto n](y)=\sigma(y)$,

and

• •

a transition relation $\Downarrow_{\_}P$ between configurations, which is defined as a big-step semantics by the inference rules illustrated in Figure 5.

We assume that for any configuration $\langle\alpha,\,\sigma_{\_}0,\,\sigma_{\_}1\rangle$ for a program $P$, the assignment $\sigma_{\_}0$ is defined for all global variables of $P$. To compute the result of a function call $f(e_{\_}1,\ldots,e_{\_}m)$ under assignments $\sigma_{\_}0,\sigma_{\_}1$ for ${\mathcal{GV}\mathit{ar}}(P)$ and ${\mathcal{V}\mathit{ar}}(e_{\_}1,\ldots,e_{\_}m)\setminus{\mathcal{GV}\mathit{ar}}(P)$, given a fresh variable $x$, we start with the configuration $\langle x~{}=~{}f(e_{\_}1,\ldots,e_{\_}m),\,\sigma_{\_}0,\,\sigma_{\_}1[x\mapsto 0]\rangle$. When $\langle x~{}=~{}f(e_{\_}1,\ldots,e_{\_}m),\,\sigma_{\_}0,\,\sigma_{\_}1[x\mapsto 0]\rangle\Downarrow_{\_}P\langle\epsilon,\,\sigma_{\_}0^{\prime},\,\sigma_{\_}1^{\prime}\rangle$ holds, the execution halts and the result of the function call $f(e_{\_}1,\ldots,e_{\_}m)$ under $\sigma_{\_}0,\sigma_{\_}1$ is $\sigma_{\_}1^{\prime}(x)$.

3 A New Approach to Transformations of Imperative Programs

In this section, using an example, we introduce a new approach to transformations of imperative programs with function calls and global variables.

3.1 The Existing Transformation of Functions Accessing Global Variables

In this section, we briefly recall the transformation of imperative programs with functions accessing global variables [6] using the program $P_{1}$ in Figure 3. Unlike $\mathcal{R}_{2}$ in Section 1, in the following, we do not optimize generated rewrite rules in LCTRSs in order to make it easier to understand how to precisely transform programs. The program $P_{1}$ is transformed into the following LCTRS with the sort set $\{\mathit{int},\mathit{bool},\mathit{state}\}$ and the standard integer signature $\Sigma_{\mathit{theory}}^{\mathit{int}}$ [6]:

[TABLE]

where $\mathsf{main}:\mathit{int}\Rightarrow\mathit{state}$, $\mathsf{u_{1}},\mathsf{u_{2}},\mathsf{u_{3}},\mathsf{u_{4}},\mathsf{u_{5}},\mathsf{u_{7}},\mathsf{u_{8}},\mathsf{u_{9}}:\mathit{int}\times\mathit{int}\times\mathit{int}\Rightarrow\mathit{state}$, $\mathsf{sum},\mathsf{u_{10}},\mathsf{u_{12}},\mathsf{return}:\mathit{int}\times\mathit{int}\Rightarrow\mathit{state}$, $\mathsf{u_{11}}:\mathit{int}\times\mathit{int}\times\mathit{state}\Rightarrow\mathit{state}$, and $\mathsf{u_{6}}:\mathit{int}\times\mathit{int}\times\mathit{int}\times\mathit{state}\Rightarrow\mathit{state}$. The declaration of local variable $\mathtt{z}$ of $\mathtt{sum}$ is represented by the first rule of $\mathcal{R}_{3}$, which stores the initial value $\mathsf{0}$ in the third argument of $\mathsf{u_{1}}$. The if-statement is represented by rules of $\mathsf{u_{2}}$, $\mathsf{u_{4}}$, and $\mathsf{u_{8}}$; The first rule of $\mathsf{u_{2}}$ enters the body of the then-statement if $x\leq\mathsf{0}$ holds, and the second rule of $\mathsf{u_{2}}$ enters the body of the else-statement if $x\leq\mathsf{0}$ does not hold (i.e., $\neg(x\leq\mathsf{0})$ holds); The end of the if-statement is represented by terms rooted by $\mathsf{u_{9}}$, and the rules of $\mathsf{u_{4}}$ and $\mathsf{u_{8}}$ are used to exit the bodies of the then- and else-statements, respectively.

To represent the function call sum(x - 1), the auxiliary function symbol $\mathsf{u_{6}}$ takes the term $\mathsf{sum}(x-\mathsf{1},\mathit{num})$ as the fourth argument. The function symbol $\mathsf{sum}$ takes two arguments, while the original function $\mathtt{sum}$ in the program takes one argument. This is because the global variable $\mathtt{num}$ is accessed during the execution of $\mathtt{sum}$, and we pass the value stored in $\mathit{num}$ to $\mathsf{sum}$, passing the variable itself to $\mathsf{sum}$ in the constructed rule. The rule of $\mathsf{u_{1}}$ increments the global variable $\mathtt{num}$, and thus, we include the value stored in $\mathit{num}$ in the result of $\mathsf{sum}$ by means of $\mathsf{return}(z,\mathit{num_{\_}{new}})$. The rule of $\mathsf{u_{6}}$ is used after the reduction of $\mathsf{sum}(x-\mathsf{1},\mathit{num})$, receiving the result by means of the pattern $\mathsf{return}(y,\mathit{num_{\_}{new}})$. The updated value stored in $\mathtt{num}$ is received by $\mathit{num_{\_}{new}}$, and the rule of $\mathsf{u_{6}}$ updates the global variable $\mathtt{num}$ by passing $\mathit{num_{\_}{new}}$ to the second argument of $\mathsf{u_{7}}$. We do the same for the function call sum(z) in the auxiliary function symbol $\mathsf{u_{11}}$. For the execution of the program, we have the reduction of $\mathcal{R}_{3}$ illustrated in Figure 6. Note that the global variable $\mathtt{num}$ is initialized by $\mathsf{0}$ and we started from $\mathsf{main}(\mathsf{0})$. From the reduction, we can see that the called function is the only running one under sequential execution, and others are waiting for the called function halting. The approach above to function calls and global variables is enough for sequential execution.

In the LCTRS $\mathcal{R}_{3}$ above, the function symbol $\mathsf{u_{6}}$ recursively calls $\mathsf{sum}$ in its fourth argument. For this reason, the running function is located below $\mathsf{u_{6}}$, and positions where $\mathsf{sum}$ is called are not unique. The above approach to transform function calls is very naive but not so general. For example, to model parallel execution, a value stored in a global variable does not have to be passed to a particular function or a process because another function or process may access the global variable.

3.2 Another Approach to Global Variables

In this section, we show another approach to the treatment of global variables.

To adapt to more general settings such as parallel execution, global variables used like shared memories should be located at fixed addresses (i.e., fixed positions of terms) because they may be accessed from two or more functions or processes. To keep values stored in global variables at fixed positions, we do not pass (values of) global variables to called functions in order to avoid locally updating global variables. To this end, we prepare a new function symbol $\mathsf{env}$ to represent the whole environment for execution, and make $\mathsf{env}$ have values stored in global variables in its arguments. In addition, we make $\mathsf{env}$ have an extra argument where functions or processes are executed sequentially.222 When we execute $n$ ($>1$) processes in parallel, we make $\mathsf{env}$ have $n$ extra arguments where the $i$-th process is executed in the $i$-th extra argument.

For example, the process of executing the above program is expressed as follows:

[TABLE]

Note that $\mathsf{env}$ has the sort $\mathit{int}\times\mathit{state}\Rightarrow\mathit{env}$, where $\mathit{env}$ is a new sort for environment. The first argument of $\mathsf{env}$ is the place where values for the global variable num are stored, and the second argument of $\mathsf{env}$ is the place where functions are executed, e.g., the main function main is called as in the above term.

We do not change the transformation of local statements—statements without accessing global variables—in function definitions. Let us consider the execution of the program, i.e., main. All the statements in main and the first statement of $\mathtt{sum}$ are local, and thus, we transform the definition of main as well as $\mathcal{R}_{3}$:

[TABLE]

The symbol $\mathsf{return}$ no longer contains values for the global variable $\mathtt{num}$. In executing the program (i.e., main), the first access to the global variable $\mathtt{num}$ is the statement “num = num + 1” in the definition of $\mathsf{sum}$. The initial term $\mathsf{env}(\mathsf{0},\mathsf{main}())$ can be reduced to $\mathsf{env}(\mathsf{0},\mathsf{u_{11}}(\mathsf{3},\mathsf{u_{1}}(\mathsf{3},\mathsf{0})))$, and thus, the first execution of the statement “num = num + 1” can be expressed by the following rewrite rule for $\mathsf{env}$:

[TABLE]

The other statements in the definition of sum are local and we transform them into the following rules, as well as $\mathcal{R}_{3}$:

[TABLE]

Unfortunately, the above rules are not enough to capture all possible executions, e.g. the second execution of “num = num + 1”, which is done by the second call of sum, is not expressed yet. Thus, we prepare the following rule:

[TABLE]

In addition, sum is further recursively called, and we need the following rule:

[TABLE]

In summary, we need similar rules for all recursive calls of $\mathtt{sum}$. The function sum may receive all the (finitely many) integers, and we need many similar rules, all of which express the increment of num. In addition, we may need other rules for the case where we add other functions calling sum into the program. More generally, the nesting of function calls cannot be fixed, and thus, along the above approach, we may need infinitely many rewrite rules. This means that the above approach is not adequate for recursive functions.

The troublesome observed by means of $P_{1}$ is caused by the fact that positions where $\mathsf{sum}$ is called are not unique in the above approach. We will show another approach to avoid this troublesome in the next section.

3.3 Using a Call Stack for Function Calls

In this section, using $P_{1}$ in Figure 3, we show a new representation of function calls for LCTRSs.

The approach to the treatment of global variables in the previous section needs finitely or infinitely many similar rules for statements accessing global variables, and we have to add other similar rules when we introduce another function that may call itself or other functions. As described at the end of the previous section, the cause of this problem is that positions where functions are called in terms rooted by $\mathsf{env}$ are not unique due to nestings of auxiliary function symbols, one of which is running and the others are waiting. A solution to fix this problem is to make such positions unique. An execution is represented as a term rooted by $\mathsf{env}$, and global variables are located at fixed positions (i.e., arguments of $\mathsf{env}$). The last argument of $\mathsf{env}$ is used for execution of user-defined functions. In the last argument, we fix positions where functions are called by using a so-called call stack. To this end, we prepare a binary function symbol $\mathsf{stack}:\mathit{state}\times\mathit{process}\Rightarrow\mathit{process}$ and a constant $\bot:\mathit{process}$ (the empty stack). To adapt to stacks, we change the sort of $\mathsf{env}$. For example, we give $\mathit{int}\times\mathit{process}\Rightarrow\mathit{env}$ to $\mathsf{env}$, and the initial term for the execution of the program is the following one:

[TABLE]

In this approach, the environment has a stack $\mathit{s}$ to execute functions by means of the form $\mathsf{env}(\ldots,\mathit{s})$. In calling a function $\mathsf{f}$ as $\mathsf{f}(\vec{t})$, we push $\mathsf{f}(\vec{t})$ as a frame for the function call to the stack $\mathit{s}$, and after the execution (successfully) halts, we pop the frame of the form $\mathsf{return}(\ldots)$ from the stack.

Along the idea above, the statements of calling functions in $P_{1}$ in Figure 3—the rules of $\mathcal{R}_{3}$ related to $\mathsf{u_{6}}$ or $\mathsf{u_{11}}$—are transformed into the following rules:

[TABLE]

The first and third rules push frames to the stack, and the second and fourth pop frames. For a term $\mathsf{env}(x_{\_}1,\ldots,x_{\_}k,\mathsf{stack}(\ldots))$, the reduction of user-defined functions is performed at the position $k+1$ of the term, where $x_{\_}1,\ldots,x_{\_}k$ are global variables. For this reason, statements accessing global variables can be represented by the following form:

[TABLE]

Note that $s$ in the above rule is a variable. The statement “num = num + 1” in $P_{1}$—the rule of $\mathcal{R}_{3}$ to increment $\mathit{num}$—is transformed into the following rule:

[TABLE]

In summary, $P_{1}$ is transformed into the following LCTRS with the sort set $\{\mathit{int},\mathit{bool},\mathit{state},\mathit{env},\mathit{process}\}$ and the standard integer signature $\Sigma_{\mathit{theory}}^{\mathit{int}}$:

[TABLE]

For the execution of the program, we have the reduction of $\mathcal{R}_{4}$ illustrated in Figure 7.

The function symbol $\mathsf{stack}$ is a defined symbol of $\mathcal{R}_{4}$, while it looks a constructor for stacks. If we would like the resulting LCTRS to be a constructor system, rules performing “push” and “pop” for stacks may be generated as rules for $\mathsf{env}$. More precisely, we generate $\mathsf{env}(\vec{x},\mathsf{stack}(t,\mathit{s}))\to\mathsf{env}(\vec{x},\mathsf{stack}(t^{\prime},s^{\prime}))$ instead of $\mathsf{stack}(t,\mathit{s})\to\mathsf{stack}(t^{\prime},s^{\prime})$.

4 Formalizing the Transformation Using Stacks

In this section, we formalize the idea of using call stacks, which is illustrated in Section 3, showing a precise transformation of SIMP+ programs into LCTRSs.

In the following, we deal with a SIMP+ program $P$ which is of the following form:

[TABLE]

where $\alpha_{\_}1,\ldots,\alpha_{\_}{k^{\prime}}$ are statements with local-variable declarations and no function other than $\mathsf{f}_{\_}1,\ldots,\mathsf{f}_{\_}{k^{\prime}}$ is called in $\alpha_{\_}1,\ldots,\alpha_{\_}{k^{\prime}}$. Note that $\mathsf{f}_{\_}1,\ldots,\mathsf{f}_{\_}{k^{\prime}}$ may be self- or mutually recursive. We abuse integer and boolean expressions of SIMP+ programs as theory terms and formulas, respectively, over the standard integer signature $\Sigma_{\mathit{theory}}^{\mathit{int}}$. In the following, we denote the sequences $x_{\_}1,\ldots,x_{\_}k$ and $y_{\_}{i,1},\ldots,y_{\_}{i,m_{\_}i}$ by $\vec{x}$ and $\overrightarrow{y_{i}}$, respectively, and the notation $\overrightarrow{y}$ stands for $\overrightarrow{y_{i}}$ for some $i\in\{1,\ldots,k^{\prime}\}$.

First, we define an auxiliary function $\mathit{aux}_{P}$ that takes a term $t$, a statement $\beta$ with variable declarations, and a non-negative integer $i$ as input, and returns a triple $(u,\mathcal{R}_{\_}\beta,j)$ of a term $u$, a set $\mathcal{R}_{\_}\beta$ of constrained rewrite rules, and a non-negative integer $j$. The resulting rewrite rules in $\mathcal{R}_{\_}\beta$ reduce an instance of $\mathsf{env}(\vec{x},\mathsf{stack}(t,s))$ to an instance of $\mathsf{env}(\vec{x},\mathsf{stack}(u,s))$: if the instance of $\mathsf{env}(\vec{x},\mathsf{stack}(t,s))$ corresponds to a configuration $\langle\beta,\,\sigma,\,\sigma^{\prime}\rangle$, then the instance of $\mathsf{env}(\vec{x},\mathsf{stack}(u,s))$ corresponds to a configuration $\langle\epsilon,\,\sigma^{\prime\prime},\,\sigma^{\prime\prime\prime}\rangle$ such that $\langle\beta,\,\sigma,\,\sigma^{\prime}\rangle\Downarrow_{\_}P\langle\epsilon,\,\sigma^{\prime\prime},\,\sigma^{\prime\prime\prime}\rangle$. The input term $t$ is of the form either $\mathsf{f}_{\_}{k^{\prime\prime}}(\overrightarrow{y_{k^{\prime\prime}}})$ or $\mathsf{u}_{\_}{i^{\prime}}(\overrightarrow{y_{k^{\prime\prime}}},z_{\_}{k^{\prime\prime},1},\ldots,z_{\_}{k^{\prime\prime},m^{\prime}_{\_}{k^{\prime\prime}}})$ where $z_{\_}{k^{\prime\prime},1},\ldots,z_{\_}{k^{\prime\prime},m^{\prime}_{\_}{k^{\prime\prime}}}$ are locally declared variables in $\alpha_{\_}{k^{\prime\prime}}$ and $\mathsf{u}_{\_}{i^{\prime}}$ is a newly introduced function symbol with $i^{\prime}<i<j$. The resulting term $u$ is of the form of $\mathsf{u}_{\_}{j^{\prime}}(\overrightarrow{y_{k^{\prime\prime}}},z_{\_}{k^{\prime\prime},1},\ldots,z_{\_}{k^{\prime\prime},m^{\prime\prime}_{\_}{k^{\prime\prime}}})$ where $m^{\prime}_{\_}{k^{\prime\prime}}\leq m^{\prime\prime}_{\_}{k^{\prime\prime}}$, $z_{\_}{k^{\prime\prime},1},\ldots,z_{\_}{k^{\prime\prime},m^{\prime\prime}_{\_}{k^{\prime\prime}}}$ are locally declared variables in $\alpha_{\_}{k^{\prime\prime}}$, and $\mathsf{u}_{\_}{j^{\prime}}$ is a newly introduced function symbol with $i\leq j^{\prime}<j$. In the following, we denote the sequence $z_{\_}{k^{\prime\prime},1},\ldots,z_{\_}{k^{\prime\prime},m^{\prime}_{\_}{k^{\prime\prime}}}$ by $\overrightarrow{z_{k^{\prime\prime}}}$, and the sequence $e^{\prime}_{\_}1,\ldots,e^{\prime}_{\_}{m_{\_}i}$ of integer expressions by $\overrightarrow{e^{\prime}_{i}}$, and the notation $\overrightarrow{z}$ stands for $\overrightarrow{z_{k^{\prime\prime}}}$ for some $k^{\prime\prime}\in\{1,\ldots,k^{\prime}\}$.

Definition 4.1

The auxiliary function $\mathit{aux}_{P}$ is defined as follows:

• •

$\mathit{aux}_{P}(t,~{}\epsilon,~{}i)=(t,\emptyset,i)$*, *

• •

$\mathit{aux}_{P}(g(\overrightarrow{y},\overrightarrow{z}),~{}\mathtt{int}~{}z^{\prime}~{}=~{}n;~{}\beta,~{}i)=(u,\{~{}g(\overrightarrow{y},\overrightarrow{z})\to\mathsf{u}_{\_}i(\overrightarrow{y},\overrightarrow{z},n)~{}\}\cup\mathcal{R}_{\_}\beta,j)$, where

• –

$\mathit{aux}_{P}(\mathsf{u}_{\_}i(\overrightarrow{y},\overrightarrow{z},z^{\prime}),\beta,i+1)=(u,\mathcal{R}_{\_}\beta,j)$,

• •

$\mathit{aux}_{P}(g(\overrightarrow{y},\overrightarrow{z}),~{}z^{\prime}~{}=~{}e;~{}\beta,~{}i)=(u,\{~{}C[g(\overrightarrow{y},\overrightarrow{z})]\to(C[\mathsf{u}_{\_}i(\overrightarrow{y},\overrightarrow{z})])\{z^{\prime}\mapsto e\}~{}\}\cup\mathcal{R}_{\_}\beta,j)$* if $e$ is an integer expression, where*

• –

if $\{\vec{x}\}\cap(\{z^{\prime}\}\cup{\mathcal{V}\mathit{ar}}(e))\neq\emptyset$ then $C[\,]=\mathsf{env}(\vec{x},\mathsf{stack}(\Box,w))$ with a fresh variable $w\notin\{\vec{x},\overrightarrow{y},\overrightarrow{z}\}$, and otherwise $C[\,]=\Box$, and

• –

$\mathit{aux}_{P}(\mathsf{u}_{\_}i(\overrightarrow{y},\overrightarrow{z},z^{\prime}),\beta,i+1)=(u,\mathcal{R}_{\_}\beta,j)$,

• •

$\mathit{aux}_{P}(g(\overrightarrow{y},\overrightarrow{z}),~{}z^{\prime}~{}=~{}\mathsf{f}_{\_}{k^{\prime\prime}}(\overrightarrow{e^{\prime}_{k^{\prime\prime}}});~{}\beta,~{}i)=$**

[TABLE]

where

• –

$w,z^{\prime\prime}$* are different fresh variables not in $\{\vec{x},\overrightarrow{y},\overrightarrow{z}\}$,*

• –

if $\{\vec{x}\}\cap{\mathcal{V}\mathit{ar}}(\overrightarrow{e^{\prime}_{k^{\prime\prime}}})\neq\emptyset$ then $C[\,]=\mathsf{env}(\vec{x},\Box)$, and otherwise $C[\,]=\Box$,

• –

if $z^{\prime}\in\{\vec{x}\}$ then $C^{\prime}[\,]=\mathsf{env}(\vec{x},\Box)$, and otherwise $C^{\prime}[\,]=\Box$, and

• –

$\mathit{aux}_{P}(\mathsf{u}_{\_}{i+1}(\overrightarrow{y},\overrightarrow{z}),\beta,i+2)=(u,\mathcal{R}_{\_}\beta,j)$,

• •

$\mathit{aux}_{P}(g(\overrightarrow{y},\overrightarrow{z}),~{}\mathtt{if}(\,\varphi\,)\{\,\beta_{\_}1\,\}\mathtt{else}\{\,\beta_{\_}2\,\}~{}\beta,~{}i)=$**

[TABLE]

where

• –

$\mathit{aux}_{P}(\mathsf{u}_{\_}i(\overrightarrow{y},\overrightarrow{z}),\beta_{\_}1,i+1)=(u_{\_}1,\mathcal{R}_{\_}{\beta_{\_}1},j_{\_}1)$,

• –

$\mathit{aux}_{P}(\mathsf{u}_{\_}{j_{\_}1+1}(\overrightarrow{y},\overrightarrow{z}),\beta_{\_}2,j_{\_}1+1)=(u_{\_}2,\mathcal{R}_{\_}{\beta_{\_}2},j_{\_}2)$,

• –

if $\{\vec{x}\}\cap{\mathcal{V}\mathit{ar}}(\varphi)\neq\emptyset$ then $C[\,]=\mathsf{env}(\vec{x},\mathsf{stack}(\Box,w))$ with a fresh variable $w\notin\{\vec{x},\overrightarrow{y},\overrightarrow{z}\}$, and otherwise $C[\,]=\Box$, and

• –

$\mathit{aux}_{P}(\mathsf{u}_{\_}{j_{\_}2}(\overrightarrow{y},\overrightarrow{z}),\beta,j_{\_}2+1)=(u,\mathcal{R}_{\_}\beta,j)$,

• •

$\mathit{aux}_{P}(g(\overrightarrow{y},\overrightarrow{z}),~{}\mathtt{while}(\,\varphi\,)\{\,\alpha\,\}~{}\beta,~{}i)=$**

[TABLE]

where

• –

$\mathit{aux}_{P}(\mathsf{u}_{\_}i(\overrightarrow{y},\overrightarrow{z}),\alpha,i+1)=(u,\mathcal{R}_{\_}\alpha,j)$,

• –

if $\{\vec{x}\}\cap{\mathcal{V}\mathit{ar}}(\varphi)\neq\emptyset$ then $C[\,]=\mathsf{env}(\vec{x},\mathsf{stack}(\Box,w))$ with a fresh variable $w\notin\{\vec{x},\overrightarrow{y},\overrightarrow{z}\}$, and otherwise $C[\,]=\Box$. and

• –

$\mathit{aux}_{P}(\mathsf{u}_{\_}j(\overrightarrow{y},\overrightarrow{z}),\beta,j+1)=(u^{\prime},\mathcal{R}_{\_}\beta,j^{\prime})$,

The sorts of generated symbols are determined as follows: $\mathsf{f}_{\_}1,\ldots,\mathsf{f}_{\_}{k^{\prime}},\mathsf{u}_{\_}i,\mathsf{u}_{\_}{i+1},\ldots:\mathit{int}\times\cdots\times\mathit{int}\Rightarrow\mathit{state}$, $\mathsf{return}:\mathit{int}\Rightarrow\mathit{state}$, $\mathsf{env}:\mathit{int}\times\cdots\times\mathit{int}\times\mathit{process}\Rightarrow\mathit{env}$, $\mathsf{stack}:\mathit{state}\times\mathit{process}\Rightarrow\mathit{process}$, and $\bot:\mathit{process}$.

Using $\mathit{aux}_{P}$, the transformation illustrated in Section 3 is defined as follows.

Definition 4.2

*We define $\mathit{conv}$ by $\mathit{conv}(P)=\bigcup_{\_}{i=1}^{k^{\prime}}(\mathcal{R}_{\_}i\cup\{~{}C_{\_}i[\mathit{u}_{\_}i]\to C_{\_}i[\mathsf{return}(e_{\_}i)]~{}\})$, where $j_{\_}1=1$ 333 The third argument of $\mathit{aux}_{P}$ is used to generate new function symbols of the form $\mathsf{u}_{\_}i$. We do not have to start with $1$, and we can put any non-negative integer into the third argument of $\mathit{aux}_{P}$ in order to, e.g., avoid the introduction of the same function symbol for two different inputs.

and for each $i\in\{1,\ldots,k^{\prime}\}$,*

• •

$\mathit{aux}_{P}(\mathsf{f}_{\_}i(\overrightarrow{y_{i}}),\alpha_{\_}i,j_{\_}i)=(u_{\_}i,\mathcal{R}_{\_}i,j_{\_}{i+1})$, and

• •

if $\{\vec{x}\}\cap{\mathcal{V}\mathit{ar}}(e_{\_}i)\neq\emptyset$ then $C_{\_}i[\,]=\mathsf{env}(\vec{x},\mathsf{stack}(\Box,w))$ with a fresh variable $w\notin\{\vec{x}\}\cup{\mathcal{V}\mathit{ar}}(u_{\_}i)$, and otherwise $C_{\_}i[\,]=\Box$.

By definition, it is clear that $\mathit{conv}(P)$ is an LCTRS with the sort set $\{\mathit{int},\mathit{bool},\mathit{state},\mathit{env},\mathit{process}\}$ and the standard integer signature $\Sigma_{\mathit{theory}}^{\mathit{int}}$. Note that Definitions 4.1 and 4.2 follow the formulation in [7]. Note also that $\mathcal{R}$ is orthogonal, any term reachable from $(\mathsf{env}(\vec{x},\mathsf{stack}(\mathsf{f}_{\_}i(\overrightarrow{y_{i}}),s)))(\sigma_{\_}0\cup\sigma_{\_}1)$ with a normal form $s$ has at most one redex that is not for $\mathcal{R}_{\mathtt{calc}}$.444 More precisely, the redex of a term reachable from $(\mathsf{env}(\vec{x},\mathsf{stack}(\mathsf{f}(\overrightarrow{y}),s)))(\sigma_{\_}0\cup\sigma_{\_}1)$ is at the root position, position $k+1$, position $(k+1).1$, or position $(k+1).1.p$ for some $p$.

Since the reduction of $\mathcal{R}_{\mathtt{calc}}$ is convergent, we restrict the reduction of $\mathcal{R}_{\mathtt{calc}}$ to the leftmost one. Then, any subderivation $t\mathrel{\to^{*}_{\_}\mathcal{R}}t^{\prime}$ of a derivation from $(\mathsf{env}(\vec{x},\mathsf{stack}(\mathsf{f}_{\_}i(\overrightarrow{y_{i}}),s)))(\sigma_{\_}0\cup\sigma_{\_}1)$ has at most one pass from $t$ to $t^{\prime}$.

Example 4.3

Consider the program $P_{1}$ in Figure 3. We have that $\mathit{conv}(P_{1})=\mathcal{R}_{4}$.

Finally, we show correctness of the transformation $\mathit{conv}$. Recall that $P$ is assumed to be of the form (1). We first show two auxiliary lemmas.

Lemma 4.4

Let $\mathcal{R}$ be an LCTRS, $e$ an integer expression, $n$ an integer, and $\sigma$ an assignments for ${\mathcal{V}\mathit{ar}}(e)$. Then, $(e,\sigma)\Downarrow_{\mathrm{calc}}n$ if and only if $e\sigma\mathrel{\to^{*}_{\_}{\mathcal{R}}}n$.

*Proof. *

Trivial by the definitions of $\Downarrow_{\mathrm{calc}}$ and $\mathcal{R}_{\mathtt{calc}}$. $\Box$

Lemma 4.5** **(Correctness of $\mathit{aux}_{P}$)

*Let $\mathcal{R}=\mathit{conv}(P)$, and $\beta$ a substatement of $\alpha_{\_}i$ for some $i\in\{1,\ldots,k^{\prime}\}$ (i.e., $\beta$ appears in $\alpha_{\_}i$). Then, both of the following hold: *

1. (a)

$\mathit{aux}_{P}(t,\beta,i^{\prime})$* for any $t$ and $i^{\prime}$ is defined, and* 2. (b)

$\mathit{aux}_{P}(t,\beta,i^{\prime})$* for some $t$ and $i^{\prime}$ is computed during the computation of $\mathit{conv}(P)$.*

Suppose that $\mathit{aux}_{P}(g(\overrightarrow{y},\overrightarrow{z}),\beta,i^{\prime})$ is computed for $\mathit{conv}(P)$. Let $\mathit{aux}_{P}(g(\overrightarrow{y},\overrightarrow{z}),\beta,i^{\prime})=(u,\mathcal{R}_{\_}\beta,j)$, and $s$ be a normal form of $\mathcal{R}$, $\sigma_{\_}0,\sigma_{\_}0^{\prime}$ assignments for ${\mathcal{GV}\mathit{ar}}(P)$, and $\sigma_{\_}1,\sigma_{\_}1^{\prime}$ assignments for $\{\overrightarrow{y},\overrightarrow{z}\}\cup({\mathcal{V}\mathit{ar}}(\beta)\setminus\{\vec{x}\})$. Then, both of the following hold:

1. (c)

$\mathcal{R}_{\_}\beta\subseteq\mathcal{R}$, 2. (d)

$\langle\beta,\,\sigma_{\_}0,\,\sigma_{\_}1\rangle\Downarrow_{\_}P\langle\epsilon,\,\sigma_{\_}0^{\prime},\,\sigma_{\_}1^{\prime}\rangle$* if and only if*

[TABLE]

*Proof. *

By definition, it is clear that (a)–(c) hold. Using Lemma 4.4, the only-if and if parts of (d) can be proved by induction on the height of the inference for $\langle\beta,\,\sigma_{\_}0,\,\sigma_{\_}1\rangle\Downarrow_{\_}P\langle\epsilon,\,\sigma_{\_}0^{\prime},\,\sigma_{\_}1^{\prime}\rangle$ and the length of $\to^{*}_{\_}{\mathcal{R}}$-steps, respectively. The difference from the proof in [7] is the treatment of global variables and function calls, while [7] adopts a small-step semantics for their imperative programs. Below, we only show the case where $\beta$ is $z^{\prime}~{}=~{}\mathsf{f}_{\_}{k^{\prime\prime}}(\overrightarrow{e^{\prime}_{k^{\prime\prime}}});~{}\beta^{\prime}$ for some $k^{\prime\prime}\in\{1,\ldots,k^{\prime}\}$. Let $\mathit{aux}_{P}(g(\overrightarrow{y},\overrightarrow{z}),\beta,i^{\prime})$ return

[TABLE]

where

• •

$w,z^{\prime\prime}$ are different fresh variables not in $\{\vec{x},\overrightarrow{y},\overrightarrow{z}\}$,

• •

if $\{\vec{x}\}\cap{\mathcal{V}\mathit{ar}}(\overrightarrow{e^{\prime}_{k^{\prime\prime}}})\neq\emptyset$ then $C^{\prime}[\,]=\mathsf{env}(\vec{x},\Box)$, and otherwise $C^{\prime}[\,]=\Box$,

• •

if $z^{\prime}\in\{\vec{x}\}$ then $C^{\prime\prime}[\,]=\mathsf{env}(\vec{x},\Box)$, and otherwise $C^{\prime\prime}[\,]=\Box$, and

• •

$\mathit{aux}_{P}(\mathsf{u}_{\_}{i^{\prime}+1}(\overrightarrow{y},\overrightarrow{z}),\beta^{\prime},i^{\prime}+2)=(u,\mathcal{R}_{\_}{\beta^{\prime}},j)$,

Then, it follows from (c) that the above two rules are included in $\mathcal{R}$.

We first show the only-if part. Assume that $\langle z^{\prime}~{}=~{}\mathsf{f}_{\_}{k^{\prime\prime}}(\overrightarrow{e^{\prime}_{k^{\prime\prime}}});~{}\beta^{\prime},\,\sigma_{\_}0,\,\sigma_{\_}1\rangle\Downarrow_{\_}P\langle\epsilon,\,\sigma_{\_}0^{\prime},\,\sigma_{\_}1^{\prime}\rangle$ holds with

• •

$(e^{\prime}_{\_}i,\sigma_{\_}0\cup\sigma_{\_}1)\Downarrow_{\mathrm{calc}}n_{\_}i$ for all $1\leq i\leq m_{\_}{k^{\prime\prime}}$,

• •

$\langle\alpha_{\_}{k^{\prime\prime}},\,\sigma_{\_}0,\,\sigma_{\_}1\rangle\Downarrow_{\_}P\langle\epsilon,\,\sigma_{\_}0^{\prime\prime},\,\sigma_{\_}1^{\prime\prime}\rangle$,

• •

$(e_{\_}{k^{\prime\prime}},\sigma_{\_}0^{\prime\prime}\cup\sigma_{\_}1^{\prime\prime})\Downarrow_{\mathrm{calc}}n$, and

• •

$\langle\beta^{\prime},\,\sigma_{\_}0^{\prime\prime\prime},\,\sigma_{\_}1^{\prime\prime\prime}\rangle\Downarrow_{\_}P\langle\epsilon,\,\sigma_{\_}0^{\prime},\,\sigma_{\_}1^{\prime}\rangle$

where

• •

if $z^{\prime}\in{\mathcal{GV}\mathit{ar}}(P)$ then $\sigma_{\_}0^{\prime\prime\prime}=\sigma_{\_}0^{\prime\prime}[z^{\prime}\mapsto n]$, and otherwise $\sigma_{\_}0^{\prime\prime\prime}=\sigma_{\_}0^{\prime\prime}$, and

• •

if $z^{\prime}\in{\mathcal{GV}\mathit{ar}}(P)$ then $\sigma_{\_}1^{\prime\prime\prime}=\sigma_{\_}1$, and otherwise $\sigma_{\_}1^{\prime\prime\prime}=\sigma_{\_}1[z^{\prime}\mapsto n]$.

It follows from Lemma 4.4 and $C^{\prime}[\mathsf{stack}(g(\overrightarrow{y},\overrightarrow{z}),w)]\to C^{\prime}[\mathsf{stack}(\mathsf{f}_{\_}{k^{\prime\prime}}(\overrightarrow{e^{\prime}_{k^{\prime\prime}}}),\mathsf{stack}(\mathsf{u}_{\_}{i^{\prime}}(\overrightarrow{y},\overrightarrow{z}),w))]\in\mathcal{R}$ that

[TABLE]

By definition, $\mathit{aux}_{P}(\mathsf{f}_{\_}{k^{\prime\prime}}(\overrightarrow{y_{k^{\prime\prime}}}),\alpha_{\_}{k^{\prime\prime}},j_{\_}{k^{\prime\prime}})$ is computed, and let $\mathit{aux}_{P}(\mathsf{f}_{\_}{k^{\prime\prime}}(\overrightarrow{y_{k^{\prime\prime}}}),\alpha_{\_}{k^{\prime\prime}},j_{\_}{k^{\prime\prime}})=(u_{\_}{k^{\prime\prime}},\mathcal{R}_{\_}{\alpha_{\_}{k^{\prime\prime}}},j_{\_}{k^{\prime\prime}+1})$. Then, by definition, we have that $\mathcal{R}_{\_}{\alpha_{\_}{k^{\prime\prime}}}\cup\{~{}C_{\_}{k^{\prime\prime}}[u_{\_}{k^{\prime\prime}}]\to C_{\_}{k^{\prime\prime}}[\mathsf{return}(e_{\_}{k^{\prime\prime}})]~{}\}\subseteq\mathcal{R}$ where $C_{\_}{k^{\prime\prime}}[\,]$ is a context defined in Definition 4.2. Let $\sigma_{\_}2=\{y_{\_}1\mapsto n_{\_}1,~{}\ldots,~{}y_{\_}{m_{\_}{k^{\prime\prime}}}\mapsto n_{\_}{m_{\_}{k^{\prime\prime}}}\}$. Then, by the induction hypothesis, we have that

[TABLE]

for an arbitrary term $s^{\prime}$. Thus, we have that

[TABLE]

It follows from $C_{\_}{k^{\prime\prime}}[u_{\_}{k^{\prime\prime}}]\to C_{\_}{k^{\prime\prime}}[\mathsf{return}(e_{\_}{k^{\prime\prime}})]\in\mathcal{R}$ and Lemma 4.4 that

[TABLE]

Since $C^{\prime\prime}[\mathsf{stack}(\mathsf{return}(z^{\prime\prime}),\mathsf{stack}(\mathsf{u}_{\_}{i^{\prime}}(\overrightarrow{y},\overrightarrow{z}),w))]\to(C^{\prime\prime}[\mathsf{stack}(\mathsf{u}_{\_}{i^{\prime}+1}(\overrightarrow{y},\overrightarrow{z}),w)])\{z^{\prime}\mapsto z^{\prime\prime}\}\in\mathcal{R}$, we have that

[TABLE]

By the induction hypothesis, we have that

[TABLE]

Therefore, the claim holds.

Next, we show the if part. Assume that

[TABLE]

Then, since derivations are unique, we can let the above derivation be the following one:

[TABLE]

where

• •

$\sigma_{\_}2=\{y_{\_}1\mapsto n_{\_}1,~{}\ldots,~{}y_{\_}{m_{\_}{k^{\prime\prime}}}\mapsto n_{\_}{m_{\_}{k^{\prime\prime}}}\}$,

• •

if $z^{\prime}\in{\mathcal{GV}\mathit{ar}}(P)$ then $\sigma_{\_}0^{\prime\prime\prime}=\sigma_{\_}0^{\prime\prime}[z^{\prime}\mapsto n]$, and otherwise $\sigma_{\_}0^{\prime\prime\prime}=\sigma_{\_}0^{\prime\prime}$, and

• •

if $z^{\prime}\in{\mathcal{GV}\mathit{ar}}(P)$ then $\sigma_{\_}1^{\prime\prime\prime}=\sigma_{\_}1$, and otherwise $\sigma_{\_}1^{\prime\prime\prime}=\sigma_{\_}1[z^{\prime}\mapsto n]$.

It follows from Lemma 4.4 and the induction hypothesis that

• •

$(e_{\_}i,\sigma_{\_}0\cup\sigma_{\_}1)\Downarrow_{\mathrm{calc}}n_{\_}i$ for all $1\leq i\leq m$,

• •

$\langle\alpha_{\_}{k^{\prime\prime}},\,\sigma_{\_}0,\,\sigma_{\_}1\rangle\Downarrow_{\_}P\langle\epsilon,\,\sigma_{\_}0^{\prime\prime},\,\sigma_{\_}1^{\prime\prime}\rangle$,

• •

$(e_{\_}{k^{\prime\prime}},\sigma_{\_}0^{\prime\prime}\cup\sigma_{\_}1^{\prime\prime})\Downarrow_{\mathrm{calc}}n$, and

• •

$\langle\beta^{\prime},\,\sigma_{\_}0^{\prime\prime\prime},\,\sigma_{\_}1^{\prime\prime\prime}\rangle\Downarrow_{\_}P\langle\epsilon,\,\sigma_{\_}0^{\prime},\,\sigma_{\_}1^{\prime}\rangle$

and thus, $\langle z^{\prime}~{}=~{}\mathsf{f}_{\_}{k^{\prime\prime}}(\overrightarrow{e^{\prime}_{k^{\prime\prime}}});~{}\beta^{\prime},\,\sigma_{\_}0,\,\sigma_{\_}1\rangle\Downarrow_{\_}P\langle\epsilon,\,\sigma_{\_}0^{\prime},\,\sigma_{\_}1^{\prime}\rangle$ holds. Therefore, the claim holds. $\Box$

Correctness of $\mathit{conv}$ can easily be proved by using Lemmas 4.4 and 4.5.

Theorem 4.6** **(Correctness of $\mathit{conv}$)

Let $\mathcal{R}=\mathit{conv}(P)$, $n\in\mathbb{Z}$, $s$ a normal form of $\mathcal{R}$, $i\in\{1,\ldots,k^{\prime}\}$, $\sigma_{\_}0,\sigma_{\_}0^{\prime}$ assignments for $\vec{x}$, and $\sigma_{\_}1,\sigma_{\_}1^{\prime}$ assignments for $\overrightarrow{y_{i}}$. Then, $\langle\alpha_{\_}i,\,\sigma_{\_}0,\,\sigma_{\_}1\rangle\Downarrow_{\_}P\langle\epsilon,\,\sigma_{\_}0^{\prime},\,\sigma_{\_}1^{\prime}\rangle$ and $(e_{\_}i,\sigma_{\_}0^{\prime}\cup\sigma_{\_}1^{\prime})\Downarrow_{\mathrm{calc}}n$ if and only if $(\mathsf{env}(\vec{x},\mathsf{stack}(\mathsf{f}_{\_}i(\overrightarrow{y_{i}}),s)))(\sigma_{\_}0\cup\sigma_{\_}1)\mathrel{\to^{*}_{\_}{\mathcal{R}}}(\mathsf{env}(\vec{x},\mathsf{stack}(\mathsf{return}(n),s)))(\sigma_{\_}0^{\prime}\cup\sigma_{\_}1^{\prime})$.

*Proof. *

We first show the only-if part. Assume that $\langle\alpha_{\_}i,\,\sigma_{\_}0,\,\sigma_{\_}1\rangle\Downarrow_{\_}P\langle\epsilon,\,\sigma_{\_}0^{\prime},\,\sigma_{\_}1^{\prime}\rangle$ and $(e_{\_}i,\sigma_{\_}0^{\prime}\cup\sigma_{\_}1^{\prime})\Downarrow_{\mathrm{calc}}n$. It follows from Lemma 4.5 and $C_{\_}i[\mathit{u}_{\_}i]\to C_{\_}i[\mathsf{return}(e_{\_}i)]\in\mathcal{R}$ (where $C_{\_}i[\,]$ is a context defined in Definition 4.2) that

[TABLE]

It follows from Lemma 4.4 that $e_{\_}i(\sigma_{\_}0^{\prime}\cup\sigma_{\_}1^{\prime})\mathrel{\to^{*}_{\_}{\mathcal{R}}}n$, and thus

[TABLE]

Therefore, the only-if part holds.

Next, we show the if part. Assume that

[TABLE]

It follows from Lemmas 4.5 and 4.4 that $\langle\alpha_{\_}i,\,\sigma_{\_}0,\,\sigma_{\_}1\rangle\Downarrow_{\_}P\langle\epsilon,\,\sigma_{\_}0^{\prime},\,\sigma_{\_}1^{\prime}\rangle$ and $(e_{\_}i,\sigma_{\_}0^{\prime}\cup\sigma_{\_}1^{\prime})\Downarrow_{\mathrm{calc}}n$. Therefore, the if part holds. $\Box$

Theorem 4.6 implies that the execution of $\mathsf{f}_{\_}i(\overrightarrow{y_{i}})$ with $\sigma_{\_}0,\sigma_{\_}1$ does not halt if and only if the reduction from $(\mathsf{env}(\vec{x},\mathsf{stack}(\mathsf{f}_{\_}i(\overrightarrow{y_{i}}),s)))(\sigma_{\_}0\cup\sigma_{\_}1)$ does not terminate. This is because by the semantics, the execution of a program never halts unsuccessfully and either successfully halts or does not halt.

5 Conclusion

In this paper, we proposed a new transformation of imperative programs with function calls and global variables into LCTRSs, and proved correctness of the transformation. A direction of future work is to apply the new transformation to a sequential program and its parallelized version in order to prove their equivalence. To simplify the discussion, we considered a program executed as a single process, i.e., executed sequentially, and the introduced symbol $\mathsf{env}$ has an argument that is used for the single process (see $\mathcal{R}_{4}$ again). To adapt to parallel execution where the number of executed processes is fixed, it suffices to add arguments for all executed processes into the symbol $\mathsf{env}$. We will formalize this idea and prove the correctness of the transformation for parallel execution.

Acknowledgements

We gratefully acknowledge the anonymous reviewers for their useful comments and suggestions to improve the paper.