The B Bank:: A complete case study

We develop a Web-based banking application with cashier and automated teller machine functionality using the B formal method. The complete development including the frontend, is specified and refined to an executable application in Atelier B. Refinement between specifications and their implementations is proved mechanically. At 2'324 lines of code and 1'397 proof obligations the B Bank is not a toy;,et it is still understandable in its details. This paper aims at filling the gap in the B literature between small text book examples and the bird's eye view reports on large industrial-size developments. Furthermore, we use B from top to bottom, fully prove all obligations, and make the case study available online.