LFCS Seminar: 29 October 2019 - James Noble

Title: Holistic Specifications


Functional specifications describe what program components can do the sufficient conditions to invoke the component's operations. A client which supplies arguments meeting an operation's preconditions can invoke that operation, and obtain the associated effect. While specifications of sufficient conditions may be enough to reason about complete, unchanging programs, they cannot support reasoning about components that must be updated over time, or components must that interact with external components of possibly unknown provenance.  In this open world setting, ensuring that components are robust even when executing with buggy or malicious external code is critical.     Holistic specifications --- 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. Holistic specifications are as concerned with necessary conditions (without which an effect will not happen) as with sufficient conditions (which are enough to cause some effect).  By adopting holistic specification techniques, programmers can explicitly define what their components should not do, making it easier to write robust and reliable programs.

Joint work with Sophia Drossopoulou, Toby Murray, Mark S Miller, and Julian Mackay.

Oct 29 2019 -

LFCS Seminar: 29 October 2019 - James Noble

Speaker: James Noble

Informatics Forum G.03