Enhancing the Tractability of Rely/Guarantee Specifications in the Development of Interfering Operations
Pierre Collette, Cliff B. Jones · The MIT Press eBooks · 2000
Various forms of assumption/commitment specifications have been used to specify and reason about the interference that comes from concurrent execution; in particular, consistent and complete proof rules relating to shared state operation specifications --with rely and guarantee conditions-- have been published elsewhere. This report investigates methodological issues in the formulation of such specifications, and their way to record design decisions. This work aims at making the use of rely/guarantee conditions more tractable, both at the specification level and in the development towards code. 1 1 Introduction Formal methods based on model-oriented specifications like VDM or B are applicable to the development of sequential operations. In such approaches, state components can be common to several operations but only one operation is executed at a time. A sequential operation can then be interpreted as a binary relation on the state space and specified with pre and post condi...