Abstract
We propose a single refinement method for B, inspired directly by Gardiner and Morgan’s longstanding single complete rule for data refinement, and rendered practical by application of the current first author’s recent first-order characterisation of refinement between monotonic computations.
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
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)
Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, New York (1998)
Banach, R., Fraser, S.: Retrenchment and the B-Toolkit. In: Treharne, H., King, S., Henson, M.C., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 203–221. Springer, Heidelberg (2005)
Derrick, J.: A single complete refinement rule for Z. Journal of Logic and Computation 10(5), 663–675 (2000)
Derrick, J., Smith, G.: Using model checking to automatically find retrieve relations. In: International Refinement Workshop (Refine 2007). Electronic Notes in Theoretical Computer Science, vol. 201, pp. 155–175. Elsevier, Amsterdam (2008)
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall International, Englewood Cliffs (1976)
Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Springer, Berlin (1990)
Dunne, S.E.: A theory of generalised substitutions. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 270–290. Springer, Heidelberg (2002)
Dunne, S.E.: Introducing backward refinement into B. In: Bert, D., Bowen, J.P., King, S., Walden, M. (eds.) ZB 2003. LNCS, vol. 2651, pp. 178–196. Springer, Heidelberg (2003)
Dunne, S.E.: Chorus Angelorum. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol. 4355, pp. 19–33. Springer, Heidelberg (2006)
Gardiner, P.H.B., Morgan, C.: A single complete rule for data refinement. Formal Aspects of Computing 5, 367–382 (1993)
Jones, C.B.: Systematic Software Development Using VDM, 2nd edn. Prentice-Hall, Englewood Cliffs (1990)
Leuschel, M., Butler, M.J.: ProB: A model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003)
Leuschel, M., Butler, M.J.: Automatic refinement checking for B. In: Lau, K., Banach, R. (eds.) ICFEM 2005. LNCS, vol. 3785, pp. 345–359. Springer, Heidelberg (2005)
Lynch, N.A.: Multivalued possibility mappings. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1989. LNCS, vol. 430, pp. 519–543. Springer, Heidelberg (1990)
Woodcock, J., Davies, J.: Using Z: Specification, Refinement and Proof. Prentice Hall, Englewood Cliffs (1996)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dunne, S., Conroy, S. (2008). A Practical Single Refinement Method for B. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds) Abstract State Machines, B and Z. ABZ 2008. Lecture Notes in Computer Science, vol 5238. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-87603-8_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-87603-8_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-87602-1
Online ISBN: 978-3-540-87603-8
eBook Packages: Computer ScienceComputer Science (R0)