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

Yoshiaki Kanazawa
(Nagoya University)
Naoki Nishida
(Nagoya University)

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.

In Joachim Niehren and David Sabel: Proceedings Fifth International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2018), Oxford, England, 8th July 2018, Electronic Proceedings in Theoretical Computer Science 289, pp. 34–52.
Published: 22nd February 2019.

ArXived at: http://dx.doi.org/10.4204/EPTCS.289.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org