关于将函数的全局变量转化为逻辑约束项重写系统
On Transforming Functions Accessing Global Variables into Logically Constrained Term Rewriting Systems
摘要：
在本文中，我们提出了一种新的方法，一个命令式程序的函数调用和全局变量转换成一个逻辑约束的长期重写系统。所得到的系统用调用堆栈表示整个执行环境的转换。更准确地说，我们为整个环境准备了一个函数符号，它存储全局变量的值和一个调用堆栈作为其参数。对于一个函数调用，我们准备重写规则来将帧压入堆栈，并在执行后弹出它。任何运行的框架都位于堆栈的顶部，访问全局变量的语句由环境符号的重写规则表示。我们展示了一个精确的转换的基础上的方法，并证明其正确性。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
