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 front end, 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; yet it is still understandable in its details. The 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