Foundations for reasoning about holistic specifications

Abstract

Specifications of sufficient conditions may be enough for reasoning about complete and unchanging programs of a closed system. Nevertheless, there is no luxury of trusting external components of probably unknown provenance in an open world that may be buggy or potentially malicious. It is critical to ensure that our components are robust when cooperating with a wide variety of external components. Holistic specifications, which are concerned with sufficient and necessary conditions, could make programs more robust in an open-world setting. In this thesis, we lay the foundations for reasoning about holistic specifications. We give an Isabelle/HOL mechanization of holistic specifications focusing on object-based programs. We also pave a way to reason about holistic specifications via proving some key lemmas that we hope will be useful in the future to establish a general logic for holistic specifications.