B is a specification language by Jean-Raymond Abrial of B Core UK, Magdalen Centre, Oxford Science Park, Oxford OX4 4GA. 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 FOLDOC, used with permission. Update as needed.