Structuring Retrenchments in B by Decomposition

10 years 3 months ago
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...
Michael Poppleton, Richard Banach
Added 06 Jul 2010
Updated 06 Jul 2010
Type Conference
Year 2003
Where FM
Authors Michael Poppleton, Richard Banach
Comments (0)