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.

翻译：强健的模块保证只做他们应该做的事情 — — 即使存在不信任、恶意的客户,并且不仅考虑个人方法的直接行为,而且考虑从呼叫到不止一种方法的突发行为。 必要性是明确稳健性的一种语言,其依据是新的必要性操作者掌握时间影响,以及从功能规格中得出明确的稳健性规格的证据逻辑。 稳健性和实例证据在 Coq 中是机械化的。