Over-approximating (OX) program logics, such as separation logic (SL), are used for verifying properties of heap-manipulating programs: all terminating behaviour is characterised, but established results and errors need not be reachable. OX function specifications are thus incompatible with true bug-finding supported by symbolic execution tools such as Pulse and Pulse-X. In contrast, under-approximating (UX) program logics, such as incorrectness separation logic, are used to find true results and bugs: established results and errors are reachable, but there is no mechanism for understanding if all terminating behaviour has been characterised. We introduce exact separation logic (ESL), which provides fully-verified function specifications compatible with both OX verification and UX true bug-funding: all terminating behaviour is characterised, and all established results and errors are reachable. We prove soundness for ESL with mutually recursive functions, demonstrating, for the first time, function compositionality for a UX logic. We show that UX program logics require subtle definitions of internal and external function specifications compared with the familiar definitions of OX logics. We investigate the expressivity of ESL and, for the first time, explore the role of abstraction in UX reasoning by verifying abstract ESL specifications of various data-structure algorithms. In doing so, we highlight the difference between abstraction (hiding information) and over-approximation (losing information). Our findings demonstrate that, expectedly, abstraction cannot be used as freely in UX logics as in OX logics, but also that it should be feasible to use ESL to provide tractable function specifications for self-contained, critical code, which would then be used for both verification and true bug-finding.

翻译：过近似（OX）程序逻辑，例如分离逻辑（SL），用于验证堆操作程序的正确性：所有终止行为均被刻画，但已建立的结果和错误未必可达。因此，OX函数规约与符号执行工具（如Pulse和Pulse-X）所支持的真正缺陷查找不兼容。相反，欠近似（UX）程序逻辑，例如不正确分离逻辑，用于发现真实结果和缺陷：已建立的结果和错误可达，但缺乏机制判断是否刻画了所有终止行为。我们引入精确分离逻辑（ESL），它提供完全验证的函数规约，同时兼容OX验证与UX真正缺陷查找：所有终止行为均被刻画，且所有已建立的结果和错误均可达。我们证明了含互递归函数的ESL的可靠性，首次展示了UX逻辑的函数组合性。研究表明，与OX逻辑中熟悉的定义相比，UX程序逻辑需要更精细地区分内部与外部函数规约。我们探讨了ESL的表达能力，并首次通过验证多种数据结构算法的抽象ESL规约，探索了抽象在UX推理中的作用。在此过程中，我们强调了抽象（隐藏信息）与过近似（丢失信息）的区别。我们的发现表明，抽象在UX逻辑中无法像在OX逻辑中那样自由使用，但应当可行地使用ESL为自包含的关键代码提供可处理的函数规约，从而同时服务于验证与真正缺陷查找。