Tags:constrained rewriting, constrained term rewriting system, global variable, imperative program and program transformation
Abstract:
A usual idea of transforming imperative programs over the integers into rewriting systems is to transform programs into transition systems where some auxiliary function symbols are introduced to represent intermediate states. In transforming a function calling itself or others, we allow an auxiliary symbol corresponding to a function call to have an extra argument where the called function is executed, and values stored in global variables are passed to the called function as its extra arguments, and the caller receives the possibly updated values together with returned values of the called function. Such a mechanism for global variables performs well under sequential execution, but is not enough to adapt to parallel execution. In this paper, we propose a transformation of imperative programs with function calls and global variables into logically constrained term rewriting systems that represent actions of the whole execution environment with call stacks. More precisely, we prepare a function symbol for the whole environment of execution, which stores global variables and a call stack as its arguments. For a function call, we push the frame to the stack and pop it after the execution. Any running frame is executed at the top of the stack, and statements accessing global variables are represented by rewrite rules for the environment symbol.
On Transforming Functions Accessing Global Variables into Logically Constrained Term Rewriting Systems