Refining a B specification into an implementation can be a complex and time consuming process. This process can usually be separated in two distinct parts: the specification part, where the refinement is used to introduce new properties and specification details, and the implementation, where refinement is used to convert a detailed B specification into a B0 implementation. The first part requires human interaction, since it corresponds to writing the specification. However, the implementation part is more mechanical, and usually corresponds to apply known refinement schemes.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{Requet08,
author = {Antoine Requet},
editor = {Egon B{\"{o}}rger and
Michael J. Butler and
Jonathan P. Bowen and
Paul Boca},
title = {{BART:} {A} Tool for Automatic Refinement},
booktitle = {Abstract State Machines, {B} and Z, First International Conference,
{ABZ} 2008, London, UK, September 16-18, 2008. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5238},
pages = {345},
publisher = {Springer},
year = {2008},
url = {https://doi.org/10.1007/978-3-540-87603-8\_33},
doi = {10.1007/978-3-540-87603-8\_33},
timestamp = {Tue, 14 May 2019 10:00:50 +0200},
biburl = {https://dblp.org/rec/conf/asm/Requet08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}