A functional rephrasing of the assumption/ commitment specification style

The assumption/commitment (also called rely/guarantee) style has been advocated for the specification of interactive components of distributed systems. 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. One of its motivations is to achieve modularity (also called compositionality) for state transition specifications of system components. Another reason for writing specifications in this format lies in proof rules that refer to this format. 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. Finally, we discuss the methodological significance of the assumption/commitment format in the stepwise development of specifications.