The B Bank: a complete case study
Martin Büchi · 2002
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.