Structuring Retrenchments in B by Decomposition

Simple retrenchment is briefly reviewed in the B language of J.-R. Abrial [1] as a liberalisation of classical refinement, for the formal description of application developments too demanding for refinement. This work initiates the study of the structuring of retrenchment-based developments in B by decomposition. A given coarse-grained retrenchment relation between specifications is decomposed into a family of more fine-grained retrenchments. The resulting family may distinguish more incisively between refining, approximately refining, and non-refining behaviours. Two decomposition results are given, each sharpening a coarsegrained retrenchment within a particular syntactic structure for operations at concrete and abstract levels. A third result decomposes a retrenchment exploiting structure latent in both levels. The theory is ild by a simple example based on an abstract model of distributed computing, and methodological aspects are considered. Keywords decomposition, formal m...

• Type: Conference
• Year: 2003
• Where: FM
• Authors: Michael Poppleton, Richard Banach
• Keywords: Coarse-grained Retrenchment Relation, FM 2003, Retrenchment, Simple Retrenchment