A Term-Rewriting Semantics for Imperative Style Programming

TL;DR

This paper introduces a term rewriting-based imperative programming language with precise semantics, enabling correctness proofs and efficient translation into imperative languages with features like assignment, iteration, and pointers.

Contribution

It presents a novel term rewriting semantics for imperative programming, bridging the gap between formal correctness proofs and practical execution.

Findings

Language allows translation into efficient imperative code

Supports features like assignment, iteration, recursion, and pointers

Facilitates correctness proofs alongside execution

Abstract

Term rewriting systems have a simple syntax and semantics and facilitate proofs of correctness. However, they are not as popular in industry or academia as imperative languages. We define a term rewriting based abstract programming language with an imperative style and a precise semantics allowing programs to be translatable into efficient imperative languages, to obtain proofs of correctness together with efficient execution. This language is designed to facilitate translations into correct programs in imperative languages with assignment statements, iteration, recursion, arrays, pointers, and side effects. It can also be used in place of a pseudo-programming language to specify algorithms.