Modeling an Algebraic Stepper
Modeling an Algebraic Stepper
复制标题
代数步进器建模
DOI：
10.1007/3-540-45309-1_21
复制
发表时间：
2001
影响因子：
4.8
通讯作者：
M. Felleisen
中科院分区：
文献类型：
--
作者：
John Clements;M. Flatt;M. Felleisen
程序员依赖于他们编程环境中工具的正确性。过去，语义学家一直在研究编译器和编译器分析的正确性，这是最重要的工具。在本文中，我们认为其他工具，如调试器和步进器，也应该使用语义模型，并且使用这些模型可以帮助开发这些工具。
我们的具体起点是我们的方案编程环境DrSolutions中的代数步进器。代数步进器通过对程序文本的代数重写来解释方案计算。程序被重写，直到它成为规范形式(如果它有规范形式的话)。规范形式是最终的结果。
单步执行程序通过放置断点并根据堆栈上的源信息重新构造源表达式，在现有的求值器中进行操作。这种方法提出了两个问题。首先，运行时断点是否对应于约简语义的步骤？其次，调试机制是否插入了足够的信息来重新构造源表达式？
为了回答这些问题，我们开发了扩展的编译器和运行时机制的高级语义模型。我们没有将评估建模为低级机器，而是以高级归约语义对步进器实现的相关低级特征进行了建模。我们希望该方法也适用于其他基于语义的工具。
Programmers rely on the correctness of the tools in their programming environments. In the past, semanticists have studied the correctness of compilers and compiler analyses, which are the most important tools. In this paper, we make the case that other tools, such as debuggers and steppers, deserve semantic models, too, and that using these models can help in developing these tools.
Our concrete starting point is the algebraic stepper in DrScheme, our Scheme programming environment. The algebraic stepper explains a Scheme computation in terms of an algebraic rewriting of the program text. A program is rewritten until it is in a canonical form (if it has one). The canonical form is the final result.
The stepper operates within the existing evaluator, by placing breakpoints and by reconstructing source expressions from source information placed on the stack. This approach raises two questions. First, do the run-time breakpoints correspond to the steps of the reduction semantics? Second, does the debugging mechanism insert enough information to reconstruct source expressions?
To answer these questions, we develop a high-level semantic model of the extended compiler and run-time machinery. Rather than modeling the evaluation as a low-level machine, we model the relevant low-level features of the stepper's implementation in a high-level reduction semantics. We expect the approach to apply to other semantics-based tools.