Work in collaboration with Susan Eisenbach (Imperial College London), Julian Mackay (Univ. Wellington), James Noble (Univ. Wellington)
Functional specifications describe what program components can do: the sufficient conditions to invoke a component’s 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 component’s pre-conditions before calling into that 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. In this open world setting, ensuring that your component is robust even when executing with buggy or malicious external code is critical.
We propose holistic specifications, which, as their name implies, are concerned with the overall behaviour of a component, in all possible interleavings of calls to the component’s operations with those of the external code. In addition to sufficient conditions which describe what is enough to cause some effect, holistic specifications are concerned with necessary conditions, i.e., the conditions without which an effect will not happen.