构建堆操作程序的合成-扩展版
Structuring the Synthesis of Heap-Manipulating Programs - Extended Version
摘要：
本文描述了一种从分离逻辑中表达的声明性规范中综合带有指针的命令式程序的演绎方法。我们的合成算法作为输入的一对断言-一个前和一个后置条件-这描述了两个状态的符号堆，并得出一个程序，将一个状态转换为其他，由堆的形状指导。程序合成算法依赖于综合分离逻辑（SSL）的新框架，SSL概括了堆蕴涵$\mathcal{P} \vdash \mathcal{Q}$的经典概念，以将满足断言$\mathcal{P}$的堆转换为满足断言$\mathcal{Q}$的堆的可能性。合成程序表示转换蕴涵语句$\mathcal{P} \leadsto \mathcal{Q}$的证明项，并且合成过程对应于证明搜索。因此，衍生程序的正确建设，在这个意义上说，他们满足归因的前/后条件，并伴随着完整的证明推导，这可以独立检查。我们已经实现了一个证明搜索引擎的SSL形式的程序合成器称为SuSLik。为了提高效率，引擎利用SSL规则的属性，例如规则应用程序在单独堆上的可逆性和可交换性，来修剪它必须考虑的派生空间。我们解释和展示SSL的使用特征的例子，描述的SuSLik的设计，并报告我们的经验，使用它来合成一系列的基准程序操纵基于堆的链接数据结构。
英文摘要：
This paper describes a deductive approach to synthesizing imperative programs with pointers from declarative specifications expressed in Separation Logic. Our synthesis algorithm takes as input a pair of assertions---a pre- and a postcondition---which describe two states of the symbolic heap, and derives a program that transforms one state into the other, guided by the shape of the heap. The program synthesis algorithm rests on the novel framework of Synthetic Separation Logic (SSL), which generalises the classical notion of heap entailment $\mathcal{P} \vdash \mathcal{Q}$ to incorporate a possibility of transforming a heap satisfying an assertion $\mathcal{P}$ into a heap satisfying an assertion $\mathcal{Q}$. A synthesized program represents a proof term for a transforming entailment statement $\mathcal{P} \leadsto \mathcal{Q}$, and the synthesis procedure corresponds to a proof search. The derived programs are, thus, correct by construction, in the sense that they satisfy the ascribed pre/postconditions, and are accompanied by complete proof derivations, which can be checked independently. We have implemented a proof search engine for SSL in a form the program synthesizer called SuSLik. For efficiency, the engine exploits properties of SSL rules, such as invertibility and commutativity of rule applications on separate heaps, to prune the space of derivations it has to consider. We explain and showcase the use of SSL on characteristic examples, describe the design of SuSLik, and report on our experience of using it to synthesize a series of benchmark programs manipulating heap-based linked data structures.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
