STRUCTURING RETRENCHMENTS IN B
Dr Michael R Poppleton, Declarative Systems and Software Engineering Research Group, Department of Electronics and Computer Science, University of Southampton

Abstract: We review simple retrenchment as a liberalisation of classical refinement, for the formal description of application developments too demanding for refinement. Two generalisations, output and evolving retrenchment, are introduced.

This work then commences the study of the structuring of developments using retrenchment. The aim is to decompose a single, coarse-grained retrenchment into a set of finer-grained retrenchments for each layer of the "onion skin" of a broad specification that includes refining, approximately refining, and non-refining behaviour. Two decomposition theorems are given, that each sharpen a coarse retrenchment description with respect to a general operation syntactic structure at concrete and abstract levels respectively. A third theorem decomposes a retrenchment, simultaneously exploiting structure in both levels. The theory is motivated by and applied to a simple example from distributed computing, and methodological aspects are considered.

This seminar was held at the Department of Computer Science, Royal Holloway, University of London on 26 November 2002.