Evaluating the utility of a contract compositionality proof framework

Abstract: A contract in system design is a concept used for specifying behaviors of and interactions between components in complex systems. Contracts make explicit the mutual commitments between components in a system. Nyberg et al propose a contracts theory and framework for proving the correctness of a decomposition of a system specification. The aim of this project is to evaluate the utility of the framework proposed by Nyberg et al. A decomposition of a concrete system’s top-level specification, and a proof of the decomposition’s correctness using the framework is performed. Evaluating the utility is done through considering a set of criteria while performing the decomposition and proof. This study finds the contracts theory to be well suited for formalizing natural language specifications and for adapting to systems with differing requirements on detail in specifications. The framework is found to have the problem that the length and complexity of the proofs created using it scale poorly with the size and complexity of the decomposition. However, automating the proof search would render the scaling problem irrelevant. Overall, the contracts theory and framework have high utility in most regards.