Topics in Semantics-based Program Manipulation
Topics in Semantics-based Program Manipulation
复制标题
基于语义的程序操作主题
DOI：
--
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
Bernd Grobauer
中科院分区：
文献类型：
--
作者：
Bernd Grobauer
编程对现有代码的操作至少与编写新代码一样多。修改现有代码，例如使效率低下的代码运行得更快，或者在重用代码时适应新功能；分析现有代码，例如验证某些程序属性，或使用分析信息进行代码修改。基于语义的程序操作解决了程序修改和程序分析的方法，这些方法是正式定义的，因此可以根据编程语言语义进行验证。本文在基于语义的程序操作技术领域包括四篇文章：三篇文章是关于程序专门化的部分求值方法；第四篇文章讨论了一种自动成本分析的方法。部分求值通过对已知输入部分进行专门化来优化程序：仅依赖于已知输入的计算在部分求值期间执行，而依赖于未知输入的计算则产生剩余代码。例如，相对于用被解释语言编写的程序，对解释器进行部分求值将产生执行该程序所描述的计算的代码；部分求值用于消除解释开销。实际上，部分求值器充当了从被解释语言到解释器的实现语言的编译器。部分求值的编译称为第一次Futamura投影。第二个和第三个Futamura投影分别描述了在编译器生成和编译器-生成器生成中使用部分求值；两者都要求所使用的部分求值器是自适用的。本文的第一篇文章描述了如何实现面向类型的部分求值（TDPE）的第二次Futamura投影，TDPE是一种相对较新的部分求值方法：我们推导了TDPE的第二次Futamura投影的ML实现。由于“传统的”、语法导向的部分求值与TDPE之间的差异，这种推导涉及到几个概念和技术步骤。这些包括第二Futamura投影的适当配方和使TDPE适于自我应用的技术。在第二篇文章中，部分求值编译在提供目标导向求值的统一方法方面起着中心作用，这是一种建立在回溯和生成连续结果概念之上的编程语言范式。将小型目标导向语言的语义表述为一元语义——一种构建指称语义的通用方法——允许我们在概念上和形式上将各种可能的语义相互联系起来。因此，我们能够使用直观的基于列表的语义来解释目标导向的求值，同时通过部分求值使用延续语义来进行基于语义的编译。结果代码与文献中描述的优化编译器产生的代码相当。第三篇文章回顾了部分评估的成功案例之一
Programming is at least as much about manipulating existing code as it is about writing new code. Existing code is modified, for example to make inefficient code run faster, or to accommodate for new features when reusing code; existing code is analyzed, for example to verify certain program properties, or to use the analysis information for code modifications. Semantics-based program manipulation addresses methods for program modifications and program analyses that are formally defined and therefore can be verified with respect to the programming-language semantics. This dissertation comprises four articles in the field of semantics-based techniques for program manipulation: three articles are about partial evaluation, a method for program specialization; the fourth article treats an approach to automatic cost analysis. Partial evaluation optimizes programs by specializing them with respect to parts of their input that are already known: Computations that depend only on known input are carried out during partial evaluation, whereas computations that depend on unknown input give rise to residual code. For example, partially evaluating an interpreter with respect to a program written in the interpreted language yields code that carries out the computations described by that program; partial evaluation is used to remove interpretive overhead. In effect, the partial evaluator serves as a compiler from the interpreted language into the implementation language of the interpreter. Compilation by partial evaluation is known as the first Futamura projection. The second and third Futamura projection describe the use of partial evaluation for compiler generation and compiler-generator generation, respectively; both require the partial evaluator that is employed to be self applicable. The first article in this dissertation describes how the second Futamura projection can be achieved for type-directed partial evaluation (TDPE), a relatively recent approach to partial evaluation: We derive an ML implementation of the second Futamura projection for TDPE. Due to the differences between ‘traditional’, syntax-directed partial evaluation and TDPE, this derivation involves several conceptual and technical steps. These include a suitable formulation of the second Futamura projection and techniques for making TDPE amenable to self-application. In the second article, compilation by partial evaluation plays a central role for giving a unified approach to goal-directed evaluation, a programming-language paradigm that is built on the notions of backtracking and of generating successive results. Formulating the semantics of a small goal-directed language as a monadic semantics—a generic approach to structuring denotational semantics— allows us to relate various possible semantics to each other both conceptually and formally. We thus are able to explain goal-directed evaluation using an intuitive list-based semantics, while using a continuation semantics for semanticsbased compilation through partial evaluation. The resulting code is comparable to that produced by an optimized compiler described in the literature. The third article revisits one of the success stories of partial evaluation, the