A Functional Rephrasing of the Assumption/commitment Specification Style

Abstract: "The assumption/commitment (also called rely/guarantee) style has been advocated for the specification of interactive components of distributed systems. One of its motivations is to achieve modularity for state transition specifications of system components. It suggests the structuring of specifications into assumptions about the behavior of the component's environment and into commitments that are fulfilled by the component provided the environment fulfills these assumptions. We define the assumption/commitment formats for functional system specifications. In particular, we work out a canonical decomposition of system specifications following the assumption/commitment format into safety and liveness aspects. We demonstrate the format of assumption/commitment specifications by a number of examples. In particular, we discuss the methodological significance of the assumption/commitment format in the stepwise development of specifications."