Retrenchment and the B-Toolkit

  • Richard Banach
  • Simon Fraser
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3455)


An experiment to incorporate retrenchment into the B-Toolkit is described. The syntax of a retrenchment construct is given, as is the proof obligation which gives retrenchment its semantics. The practical aspects of incorporating these into the existing B-Toolkit are then investigated. It transpires that the B-Toolkit’s internal architecture is heavily committed to monolithic refinement, because of B-Method philosophy, and this restricts what can be done without a complete rebuild of the toolkit. Experience with case studies is outlined.


Proof Obligation Abstract Machine Type Check Predicate Transformer Target Machine 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abrial, J.R.: The B-Tool Reference Manual, Version 1.1. B-Core (UK) LtdGoogle Scholar
  2. 2.
    Abrial, J.R.: The B Book. Cambridge University Press, Cambridge (1996)zbMATHCrossRefGoogle Scholar
  3. 3.
    Banach, R., Cross, R.: Safety requirements and fault trees using retrenchment. In: Heisel, M., Liggesmeyer, P., Wittmann, S. (eds.) SAFECOMP 2004. LNCS, vol. 3219, pp. 210–223. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  4. 4.
    Banach, R., Jeske, C.: Output retrenchments, defaults, stronger compositions, feature engineering (2002) (Submitted)Google Scholar
  5. 5.
    Banach, R., Poppleton, M.: Retrenchment: An engineering variation on refinement. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, pp. 129–147. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  6. 6.
    Banach, R., Poppleton, M.: Sharp retrenchment, modulated refinement and simulation. Formal Aspects of Computer Science 11(5), 498–540 (1999)zbMATHCrossRefGoogle Scholar
  7. 7.
    Banach, R., Poppleton, M.: Engineering and theoretical underpinnings of retrenchment (2001) (Submitted)Google Scholar
  8. 8.
    Banach, R., Poppleton, M.: Retrenching partial requirements into system definitions: A simple feature interaction case study. Req. Eng. Journal 8, 266–288 (2002)CrossRefGoogle Scholar
  9. 9.
    Behm, P., Desforges, P., Meynadier, J.-M.: Meteor: An industrial success in formal development. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, p. 26. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  10. 10.
    Desforges, P.: Using the b-method to design safety-critical software for railway systems. Recherche et Developpements - Fatis Marquant 97 (1998)Google Scholar
  11. 11.
    Essame, D.: Handling safety critical requirements in system engineering using the b formal method. In: Heisel, M., Liggesmeyer, P., Wittmann, S. (eds.) SAFECOMP 2004. LNCS, vol. 3219, p. 115. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  12. 12.
    Fraser, S.: Mechanised Support for Retrenchment in the B-Toolkit, Master’s thesis, School of Computer Science, University of Manchester (2004)Google Scholar
  13. 13.
    Fraser, S.: Specifications, Proof Obligations and Proofs Supporting a Case Study of Retrenchment in the B-Toolkit (2004) Available online at,
  14. 14.
    Haughton, H., Lano, K.: Specification in B: An Introduction Using the B-Toolkit. Imperial College Press, London (1996)Google Scholar
  15. 15.
    Poppleton, M., Banach, R.: Retrenchment: Extending the reach of refinement. In: Proc. ASE 1999, pp. 158–165. IEEE, Los Alamitos (1999)Google Scholar
  16. 16.
    Poppleton, M., Banach, R.: Controlling control systems: An application of evolving retrenchment. In: Bert, D., P. Bowen, J., C. Henson, M., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 42–61. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  17. 17.
    Schneider, S.: The B-Method: An Introduction. Palgrave (2001)Google Scholar
  18. 18.
    Sekerinski, E., Sere, K. (eds.): Program Development by Refinement. Springer, Heidelberg (1999)zbMATHGoogle Scholar
  19. 19.
    Wordsworth, J.B.: Software Engineering with B. Addison-Wesley, Reading (1996)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Richard Banach
    • 1
  • Simon Fraser
    • 1
  1. 1.Department of Computer ScienceUniversity of ManchesterManchesterUK

Personalised recommendations