Last updated 27.03.13.

Retrenchment was introduced to address some of the perceived limitations of formal, model based refinement, for situations in which refinement might be regarded as desirable in principle, but turned out to be unusable, or nearly unusable, in practice.

For an introduction to retrenchment, you are invited to look at the retrenchment reference tutorial below.

Live performances of suitable extracts from the reference tutorial can be arranged with the authors according to the needs of any given occasion. For private performances in the comfort of your own workstation: ensure you can see pdf, click the link below, select full screen mode, position your fingers over the arrow keys, and enjoy the show. (If that's too melodramatic, there is a 4-up printable version, with all the overlays taken out, in ps and pdf, at the link alongside.)

Retrenchment: an overview ..................... 4-up printable: ps / pdf

Supplementing the reference tutorial is a slideshow on the application of retrenchment to the Mondex Electronic Purse, a real world application formally developed using Z refinement, but which nevertheless furnishes a number of excellent "retrenchment opportunities" according to its lead author. (These are issues that were not treated in an ideal manner in the development due to the exigencies of refinement, but which can be approached more honestly using retrenchment.) Printable 4-up ps and pdf alongside.

Retrenchment and Mondex ..................... 4-up printable: ps / pdf

(For an introduction to the Mondex development see Susan Stepney's Smartcard web page in general, and the slideshow The Mondex purse Z refinement in particular.)

Most publications on retrenchment so far are co-authored by Richard Banach and so appear on my 'Recent Publications' page located via Richard Banach's homepage.

While detailed comments on individual papers are inappropriate, it is worth pointing out the presence of a series of papers that attempt to give a 'from scratch' development of retrenchment, written with some of the wisdom of experience, and in a consistent style, for those wanting a presentation more technically thoroughgoing than the tutorial. They are all on my publications page, and the first few in the series are:

*Engineering and Theoretical Underpinnings of Retrenchment.*

R. Banach, M. Poppleton, C. Jeske, S. Stepney

Sci. Comp. Prog., **67**, 301-329, (2007)

Preprint: Retrench.Underpin.ps.gz .......... Retrench.Underpin.pdf

(This paper, started in about 1999, gives an overview of motivations for
introducing retrenchment, surveys key issues, and overviews two case studies:
on digital control redesign, and on the Mondex Purse. This final version dates
from the end of 2005, essentially.)

*Composition Mechanisms for Retrenchment.*

R. Banach, C. Jeske, M. Poppleton

J. Log. Alg. Prog., **75**, 209-229, (2008)

Preprint: Retrench.Composition.ps.gz .......... Retrench.Composition.pdf

(Various composition mechanisms (vertical, horizontal, dataflow, fusion, etc.)
are examined from a uniform perspective, bringing out their similarities.)

*Model Based Refinement and the Design of Retrenchments.*

R. Banach

Preprint: Retrench.Designs.ps.gz .......... Retrench.Designs.pdf

(The ideas in the `Underpinnings' paper are instantiated as retrenchment
designs for Z, B, Event-B, VDM, RAISE, I/O-Automata, TLA+.)

*Retrenchment and Refinement Interworking: the Tower Theorems.*

R. Banach, C. Jeske

Math. Struc. Comp. Sci. (to appear)

Preprint: Retrench.Tower.ps.gz .......... Retrench.Tower.pdf

(A considered reappraisal and simplification of the results first demonstrated
in Jeske's thesis (below). The present theorems are much easier to mechanise.)

*Stronger Compositions for Retrenchments.*

R. Banach, C. Jeske

J. Log. Alg. Prog., **79**, 215-232, (2010)

Preprint: Retrench.Strong.Comp.ps.gz .......... Retrench.Strong.Comp.pdf

Preprint including full proofs: Retrench.Strong.Comp.FULL.ps.gz .......... Retrench.Strong.Comp.FULL.pdf

(Formerly dealing with output retrenchments, defaults, stronger compositions,
and also feature engineering, the scope has been cut down in this final
version. Now it focuses on stronger notions of vertical composition. The
"FULL" preprint includes an appendix containing proofs omitted from the
journal version.)

*Simple Feature Engineering via Neat Default Retrenchments.*

R. Banach, C. Jeske

J. Log. Alg. Prog., **80**, 453-480, (2011)

Preprint: Retrench.Feature.ps.gz .......... Retrench.Feature.pdf

(An expanded treatement of the feature engineering material previously
included in the "Stronger Compositions" paper.)

*Retrenchment and System Properties.*

R. Banach

Preprint: Retrench.Props.ps.gz .......... Retrench.Props.pdf

(System properties (characterised as sets of (sequences of) execution
fragments) and their mappings via retrenchment's bespoke simulation notion,
are examined from the semantic standpoint.)

In addition to the above, it is worth pointing out some papers in the
literature that deal with the Mondex "retrenchment opportunities",
surveyed in the tutorial above. The first is an overview, the rest
deal with individual "opportunities".

*The Mondex Purse: Requirements and Retrenchments.*

R. Banach

Preprint: Retrench.Mondex.OvView.ps.gz .......... Retrench.Mondex.OvView.pdf

*Retrenching the Purse: The Balance Enquiry Quandary,
and Generalised and (1,1) Forward Refinements.*

R. Banach, C. Jeske, M. Poppleton, S. Stepney

Fund. Inf. **77**, 29-69, (2007)

Preprint: Retrench.Mondex.Bal.ps.gz .......... Retrench.Mondex.Bal.pdf

*Retrenching the Purse: Finite Sequence Numbers,
and the Tower Pattern.*

R. Banach, M. Poppleton, C. Jeske, S. Stepney

Proc. FM-05, LNCS **3582**, 382-398, (2005)

J. Fitzgerald, I. Hayes, A. Tarlecki (eds.),

Preprint: Retrench.Mondex.Seq.ps.gz .......... Retrench.Mondex.Seq.pdf

*Retrenching the Purse: Finite Exception Logs, and Validating the Small.*

R. Banach, C. Jeske, M. Poppleton, S. Stepney

Proc. IEEE/NASA SEW30-06, 234-245, (2006),

M. Hinchey (ed.),

Preprint: Retrench.Mondex.Log.ps.gz .......... Retrench.Mondex.Log.pdf

*Retrenching the Purse: Hashing Injective CLEAR Codes,
and Security Properties.*

R. Banach, C. Jeske, M. Poppleton, S. Stepney

Proc. IEEE ISOLA-06, 82-90 (2007),

T. Margaria, B. Steffen (eds.),

Preprint: Retrench.Mondex.Hash.ps.gz .......... Retrench.Mondex.Hash.pdf

*Coarse Grained Retrenchment and the Mondex Denial of Service Attacks.*

R. Banach

Proc. IEEE TASE-09, 103-110, (2009),

W. Chin, S. Qin (eds.),

Preprint: Retrench.Mondex.CG.DOS.ps.gz .......... Retrench.Mondex.CG.DOS.pdf

Mike Poppleton's Publications Page

Czeslaw Jeske's PhD Thesis, the machinery behind the *Tower Pattern*.

Simon Fraser's PhD Thesis, on the experimental *Frog Toolkit*.