A Term-Rewriting Semantics for Imperative Style Programming
This work addresses the gap between formal verification and practical programming for developers and researchers, though it appears incremental as it builds on existing term rewriting concepts.
The authors tackled the challenge of combining the proof-friendly nature of term rewriting systems with the efficiency and popularity of imperative programming by defining a term rewriting-based abstract language with imperative style and precise semantics, enabling both correctness proofs and efficient execution.
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.