Method B for the specification and realization of proven software and mission-critical systems

It is not the intention of this article that the reader should know everything there is to know about the B method; that would be impossible and pretentious. The B-BOOK – Assigning Programs to Meanings by Jean-Raymond ABRIAL, the inventor of the B-method, which is the basis of the B-language, already runs to over 750 pages and is based on a wealth of mathematical and logical knowledge. The aim here is simply to shed some light on the main concepts behind this method, so that we can better assess it. The mathematical aspects, though essential, will not be over-developed. The discussion will always remain fairly general, sometimes deliberately simplifying to remain understandable.