Abstract
Simple retrenchment is briefly reviewed in the B language of J.-R. Abrial [1] as a liberalization 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 coarse-grained 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 illustrated by a simple example based on an abstract model of distributed computing, and methodological aspects are considered.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)
Back, R.J.R., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, Heidelberg (1998)
Back, R.J.R., Butler, M.: Fusion and simultaneous execution in the refinement calculus. Acta Informatica 35, 921–949 (1998)
Back, R.J.R., Sere, K.: Superposition refinement of reactive systems. Formal Aspects of Computing 8(3), 324–346 (1996)
Banach, R.: Maximally abstract retrenchments. In: Proc. IEEE ICFEM2000, York, August 2000, pp. 133–142. IEEE Computer Society Press, Los Alamitos (2000)
Banach, R., Jeske, C.: Output retrenchments, defaults, stronger compositions, feature engineering (2002) (submitted), http://www.cs.man.ac.uk/~banach/some.pubs/Retrench.Def.Out_OnlinePDF.pdf
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)
Banach, R., Poppleton, M.: Sharp retrenchment, modulated refinement and simulation. Formal Aspects of Computing 11, 498–540 (1999)
Banach, R., Poppleton, M.: Retrenchment, refinement and simulation. In: Bowen, J.P., Dunne, S., Galloway, A., King, S. (eds.) B 2000, ZUM 2000, and ZB 2000. LNCS, vol. 1878, p. 304. Springer, Heidelberg (2000)
Banach, R., Poppleton, M.: Model based engineering of specifications by retrenching partial requirements. In: Proc. MBRE 2001: IEEE Workshop on Model- Based Requirements Engineering, University of California, San Diego, November 2001. IEEE Press, Los Alamitos (2001)
Banach, R., Poppleton, M.: Engineering and theoretical underpinnings of retrenchment (2002) (submitted), http://www.cs.man.ac.uk/~banach/some.pubs/Retrench.Underpin_OnlinePDF.pdf
Banach, R., Poppleton, M.: Retrenching partial requirements into system definitions: A simple feature interaction case study. Requirements Engineering Journal 8(2), 22 (2003)
de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press, Cambridge (1998)
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)
Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12(10), 576–583 (1969)
Katz, S.: A superimposition control construct for distributed systems. ACM TPLAN 15(2), 337–356 (1993)
Poppleton, M., Banach, R.: Retrenchment: extending the reach of refinement. In: ASE 1999: 14th IEEE International Conference on Automated Software Engineering, October 1999, pp. 158–165. IEEE Computer Society Press, Los Alamitos (1999)
Poppleton, M., Banach, R.: Retrenchment: Extending refinement for continuous and control systems. In: Proc. IWFM 2000, NUI Maynooth, July 2000. Springer Electronic Workshop in Computer Science Series. Springer, Heidelberg (2000)
Poppleton, M., Banach, R.: Controlling control systems: An application of evolving retrenchment. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, p. 42. Springer, Heidelberg (2002)
Poppleton, M.R.: Formal Methods for Continuous Systems: Liberalising Refinement in B. PhD thesis, Department of Computer Science, University of Manchester (2001)
Schneider, S.: The B-Method. Palgrave Press (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Poppleton, M., Banach, R. (2003). Structuring Retrenchments in B by Decomposition. In: Araki, K., Gnesi, S., Mandrioli, D. (eds) FME 2003: Formal Methods. FME 2003. Lecture Notes in Computer Science, vol 2805. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45236-2_44
Download citation
DOI: https://doi.org/10.1007/978-3-540-45236-2_44
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40828-4
Online ISBN: 978-3-540-45236-2
eBook Packages: Springer Book Archive