B specification language

For people who check facts

B, is a specification language used in the development and analysis of computer software. It was developed by Jean-Raymond Abrial of B Core UK, Oxford, England. B is related to Z and supports development of C code from specifications. B has been used in major safety-critical system specifications in Europe, and is currently attracting increasing interest in industry. It has robust, commercially available tool support for specification, design, proof and code generation.

The method of software development based on B is known as the B method.

Compared to Z, B is more low-level and more focused on how computers actually work than on abstract mathematical theories -- hence it is more straightforward to implement a specification written in B than one in C.

This article was originally based on material from the Free On-line Dictionary of Computing and is used with permission under the GFDL.