论文标题
命令风格编程的术语练习语义
A Term-Rewriting Semantics for Imperative Style Programming
论文作者
论文摘要
术语重写系统具有简单的语法和语义，并促进了正确性的证明。但是，它们在行业或学术界并不像命令式语言那样受欢迎。我们定义了一种基于术语重写的抽象编程语言，具有命令性的样式和精确的语义，允许程序可以翻译成有效的命令式语言，以获得正确性的证明以及有效的执行。该语言旨在促进用作业，迭代，递归，阵列，指针和副作用的命令语言中正确的程序翻译成正确的程序。它也可以代替伪编程语言来指定算法。
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.
