5. Current advantages of method B over other methods

The B method, while not the only formal method, nor probably the most effective for all the aspects encountered in projects, has definite advantages on a number of points. Firstly, it provides a single method for specifying, designing and proving. It is therefore not necessary to model the software specification in order to prove it, as such modeling can lead to contradictions linked either to the interpretation that has been made of it, or to the limits and constraints of the model itself. It has proved highly effective for software that is not particularly simple, and this effectiveness tends to improve as experience is gained in designing other systems. This experience may relate to the architecture and organization of modules, to the accumulation of new, more efficient theorems increasing the percentage of proofs performed automatically, to a better choice of proof strategy facilitating...