一句话：提出首个针对含局部变量和按值调用参数机制的递归过程偏正确性的可靠且相对完备 Hoare 逻辑，证明长度与程序规模成线性。
本文研究递归过程在局部变量和按值调用参数机制下的 Hoare 逻辑推理问题。已有 Hoare 逻辑虽被广泛研究，但据作者称尚不存在同时处理这些特性、且证明长度与程序规模线性的可靠且相对完备系统。论文提出这样的 Hoare 逻辑，用于刻画递归过程的偏正确性，并支持合约形式的规范。其证明规则可组合地处理局部变量与按值调用参数传递，保证证明复杂度随程序长度线性增长；同时给出系统的可靠性、相对完备性，并讨论推理的复杂性。该工作填补了按值调用递归过程程序验证的一个空白。
We provide a sound and relatively complete Hoare logic for reasoning about partial correctness of recursive procedures in presence of local variables and the call-by-value parameter mechanism and in which the correctness proofs support contracts and are linear in the length of the program. We argue that in spite of the fact that Hoare logics for recursive procedures were intensively studied, no such logic has been proposed in the literature.
@article{paperbot1211,
title = {Completeness and Complexity of Reasoning about Call-by-Value in Hoare Logic},
author = {Frank S. de Boer and Hans-Dieter A. Hiep},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {43},
number = {4},
year = {2021},
doi = {10.1145/3477143}
}