论文标题
鲁棒性的必要条件
Necessity Specifications for Robustness
论文作者
论文摘要
强大的模块保证只能做他们应该做的事情 - 即使在不受信任，恶意客户的存在的情况下，不仅要考虑单个方法的直接行为，而且考虑到从呼叫到多种方法的新兴行为。必要性是一种基于捕获时间含义的新颖必要性操作员的语言，并且是从功能规范中获得明确鲁棒性规范的证明逻辑。稳健性和示例性证明是在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.
