B-Method

EN Texto em inglês Ainda não há artigo no teu idioma: trecho em inglês.

The B-Method is a method of software development based on B, a tool-supported formal method based on an abstract machine notation, used in the development of computer software. Compared to the Z notation, B is slightly more low-level and more focused on refinement to code rather than just formal specification — hence it is easier to correctly implement a specification written in B than one in Z. In particular, there is good tool support for this. The same language is used in specification, design, and programming. Mechanisms include encapsulation and data locality. B was originally developed in the 1980s by Jean-Raymond Abrial in France and the UK. B is related to the Z notation (also originated by Abrial) and supports the development of programming language code from specifications. B has been used in major safety-critical system applications in Europe (such as the automatic Paris Métro lines 14 and 1 and the Ariane 5 rocket). It has robust, commercially available tool support for specification, design, proof and code generation. From the late 1980s, Ib Holm Sørensen (1949–2012) was central to the development of the B-Method, having previously also worked on the early development of the Z notation. He left the Oxford University Computing Laboratory to lead a team for BP Research and to develop the B-Toolkit, providing tool support for the B-Method.