一种用于指针程序综合的简明只读规范--扩展版
Concise Read-Only Specifications for Better Synthesis of Programs with Pointers -- Extended Version
摘要：
在程序合成中，在简洁和强大的规范之间有一个众所周知的权衡：如果一个规范太冗长，它可能比程序更难写;如果它太弱，合成的程序可能不符合用户的意图。在这项工作中，我们探讨使用注释限制内存访问权限的程序合成，并表明，他们可以使规范更强大，同时保持令人惊讶的简洁。具体来说，我们增强了合成分离逻辑（SSL），一个框架，用于合成堆操作程序，只读借用的逻辑机制。我们观察到，这种简约和保守的SSL扩展在几个方面有利于合成，使其更具（a）表达性（以适度的注释开销实现更强的正确性保证），（b）有效（它产生更简洁和更易于阅读的程序），（c）高效（更快的合成），（d）鲁棒性（合成效率受搜索启发式选择的影响较小）。我们解释的直觉，并提供正式的治疗只读借用。我们证实了索赔（a）-（d）通过描述我们的量化评估的一系列标准的基准规格的各种堆操纵程序的感知合成实现。
英文摘要：
In program synthesis there is a well-known trade-off between concise and strong specifications: if a specification is too verbose, it might be harder to write than the program; if it is too weak, the synthesised program might not match the user's intent. In this work we explore the use of annotations for restricting memory access permissions in program synthesis, and show that they can make specifications much stronger while remaining surprisingly concise. Specifically, we enhance Synthetic Separation Logic (SSL), a framework for synthesis of heap-manipulating programs, with the logical mechanism of read-only borrows. We observe that this minimalistic and conservative SSL extension benefits the synthesis in several ways, making it more (a) expressive (stronger correctness guarantees are achieved with a modest annotation overhead), (b) effective (it produces more concise and easier-to-read programs), (c) efficient (faster synthesis), and (d) robust (synthesis efficiency is less affected by the choice of the search heuristic). We explain the intuition and provide formal treatment for read-only borrows. We substantiate the claims (a)--(d) by describing our quantitative evaluation of the borrowing-aware synthesis implementation on a series of standard benchmark specifications for various heap-manipulating programs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
