Holistic Specifications for Robust Programs

Functional specifications describe what program components can do: the sufficient conditions to invoke components' operations. They allow us to reason about the use of components in a closed world setting, where components interact with known client code, and where the client code must establish the appropriate pre-conditions before calling into a component. Sufficient conditions are not enough to reason about the use of components in an open world setting, where components interact with external code, possibly of unknown provenance, and where components 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 Chainmail specification language for writing holistic specifications that focus on necessary conditions (as well as sufficient conditions). We give a formal semantics for Chainmail, and discuss several examples. The core of Chainmail has been mechanised in the Coq proof assistant.