一句话：提出 Necessity 语言，用必要性算子刻画时序蕴含，从功能规约推导健壮性规约并在 Coq 中机械化验证可靠性。
健壮模块需在存在不可信恶意客户端时仍只做其应做之事，且不仅要考虑单个方法的直接行为，还要考虑多方法调用组合所涌现的行为。现有功能规约无法表达此类性质。本文提出 Necessity 规约语言，其核心是刻画时序蕴含的新型必要性算子，并给出一个证明逻辑，可从功能规约自动导出显式的健壮性规约。可靠性（soundness）与一个示例证明已在 Coq 中机械化验证。
Robust modules guarantee to do only what they are supposed to do – even in the presence of untrusted malicious clients, and considering not just the direct behaviour of individual methods, but also the emergent behaviour from calls to more than one method. Necessity is a language for specifying robustness, based on novel necessity operators capturing temporal implication, and a proof logic that derives explicit robustness specifications from functional specifications. Soundness and an exemplar proof are mechanised in Coq.
@article{paperbot1458,
title = {<i>Necessity</i>
specifications for robustness},
author = {Julian Mackay and Susan Eisenbach and James Noble and Sophia Drossopoulou},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA2},
year = {2022},
doi = {10.1145/3563317}
}