Personal tools
You are here: Home Events LFCS Seminars-Folder LFCS Seminars LFCS seminar: James Noble: Holistic Specifications

LFCS seminar: James Noble: Holistic Specifications

— filed under: ,

  • LFCS Seminar
  • Upcoming events
When Oct 29, 2019
from 04:00 PM to 05:00 PM
Where G.03
Add event to calendar vCal

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.

Document Actions