Rodin Handbook


4.1.3 What is the difference between Event-B and the B method?

Event-B (2.2.4) is derived from the B method. Both notations have the same inventor, and share many common concepts (set-theory, refinement, proof obligations, etc.). However, they are used for quite different purposes. The B method is devoted to the development of correct by construction software, while the purpose of Event-B is used to model full systems (including hardware, software and environment of operation).

Event-B and the B method use mathematical languages which are similar but do not match exactly (in particular, operator precedences are different).