论文标题
强大程序的整体规格
Holistic Specifications for Robust Programs
论文作者
论文摘要
功能规范描述了哪些程序组件的工作：调用组件操作的足够条件。它们使我们能够在封闭的世界设置中使用组件，其中组件与已知客户端代码进行交互，以及客户端代码在拨打组件之前必须建立适当的预条件。 足够的条件不足以推理在开放世界中使用组件的使用，该组件与外部代码相互作用，可能是未知的出处，以及组件本身随着时间的推移而发展的何处。在这个开放的世界环境中，我们还必须考虑必要的条件，即，没有效果的条件是什么。 在本文中，我们提出了语言链邮件，用于编写关注必要条件（以及足够条件）的整体规格。我们为\ Chainmail提供正式的语义。 Chainmail的核心已在COQ证明助手中进行了机械化。
Functional specifications describe what program components do: the sufficient conditions to invoke a component's operations. They allow us to reason about the use of components in the closed world setting, where the component interacts with known client code, and where the client code must establish the appropriate pre-conditions before calling into the component. Sufficient conditions are not enough to reason about the use of components in the open world setting, where the component interacts with external code, possibly of unknown provenance, and where the component itself may evolve over time. In this open world setting, we must also consider the necessary} conditions, i.e, what are the conditions without which an effect will not happen. In this paper we propose the language Chainmail for writing holistic specifications that focus on necessary conditions (as well as sufficient conditions). We give a formal semantics for \Chainmail. The core of Chainmail has been mechanised in the Coq proof assistant.
