将一种操作语义抽象为有限自动机
Abstracting an operational semantics to finite automata
摘要：
命令式程序的小步操作语义的描述与有限自动机的语义有明显的相似性，因此定义一个从语义到自动机的抽象映射并证明一个模拟性质似乎是容易的。本文的目的是确定原因简单的证明打破，其中工件的语义，导致口吃的模拟步骤。然后，我们提出了一个语义的基础上的拉链数据结构，与直接解释的评价导航的语法树。然后通过等价类构造来定义抽象函数。
英文摘要：
There is an apparent similarity between the descriptions of small-step operational semantics of imperative programs and the semantics of finite automata, so defining an abstraction mapping from semantics to automata and proving a simulation property seems to be easy. This paper aims at identifying the reasons why simple proofs break, among them artifacts in the semantics that lead to stuttering steps in the simulation. We then present a semantics based on the zipper data structure, with a direct interpretation of evaluation as navigation in the syntax tree. The abstraction function is then defined by equivalence class construction.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
