Holistic Specifications for Robust Programs
Sophia Drossopoulou, James Noble, Julian Mackay, Susan Eisenbach · Lecture notes in computer science · 2020
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 $${\mathcal {C}}$$ hainmail specification language for writing holistic specifications that focus on necessary conditions (as well as sufficient conditions). We give a formal semantics for $${\mathcal {C}}$$ hainmail, and discuss several examples. The core of $${\mathcal {C}}$$ hainmail has been mechanised in the Coq proof assistant.