A Discipline of B

Despite the evident progress in the evolution of formal methh ods, they are still very diicult to use. One reason is the lack of paradigms explaining how to make a good use of a particular method. We try to explain some of these paradigms in the case of the B method and exemm plify them in the speciication and the implementation of an Automatic Teller machine.