一句话：提出用于对象能力与封装限制外部调用效应的断言、规约与 Hoare 逻辑，并证明其可靠性。
现代软件中可信内部代码与不可信外部代码紧密交织；即使外部代码不可信甚至不可用，程序也需推理其调用可能产生的效应。论文针对依赖封装与对象能力（object capabilities）来限制外部调用效应的内部代码，提出新的能力访问断言、限制效应的规约，以及一套 Hoare 逻辑，用于验证模块在调用外部代码时仍满足其规约。作者通过一个贯穿示例展示方法并给出机器化证明，同时证明该 Hoare 逻辑的可靠性（soundness）。
In today’s complex software, internal trusted code is tightly intertwined with external untrusted code. To reason about internal code, programmers must reason about the potential effects of calls to external code, even though that code is not trusted and may not even be available. The effects of external calls can be limited if internal code is programmed defensively, limiting potential effects by limiting access to the capabilities necessary to cause those effects. This paper addresses the specification and verification of internal code that relies on encapsulation and object capabilities to limit the effects of external calls. We propose new assertions for access to capabilities, new specifications for limiting effects, and a Hoare logic to verify that a module satisfies its specification, even while making external calls. We illustrate the approach though a running example with mechanised proofs, and prove soundness of the Hoare logic.
@article{paperbot2889,
title = {Reasoning about External Calls},
author = {Sophia Drossopoulou and Julian Mackay and Susan Eisenbach and James Noble},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763064}
}