A short introduction to B

From ClearSy Tools

This is intended to to be a really short introduction to B, as many resources are already available on the web. The reader would check for example [1].

key ideas

 B is a language for specifying, designing and coding  

• When you program in C for example, you declare your variables, you give them a type and an initial value, then you define your functions, their name, their signature then their content (the algorithm). Finally you assemble your functions to obtain your program.
  

When you model in B, you are invited to give your variables more than a type (i.e. constraints ^[1] among variables for example) and to define what services your functions are supposed to deliver instead of how to deliver them.

• The B language is composed of "several", close languages: one for specifying and one for coding. The differences are based on common sense:
  • in the specification language, "programming features" like sequencing, loops, etc are forbidden. The developer may use "abstract" elements like sets, and set-based operations (intersection, union, etc).
  • in the coding language, "programming features" are mandatory. Abstract sets are prohibited. Every element should have an implementable type.

• Implentable types supported by B are translator-dependent. The basic types are boolean, integer, arrays of boolean or interger. Array of array may be supported. Real numbers are not supported for proof reason.

 B is a language for proving  

• Using theorem provers provided by b4free ^[2] or Atelier B ^[3] tools, the B developer aims at obtaining a 100% proved model. In this case, the implementation is considered to comply with its specification and no further testing is required.

• On the other hand, B suffers several restrictions, compared to programming languages like C, as the main objective is not to have the human developer to feel confortable with the language but to ensure that the model is sound. In particular, a variable has to be implemented in a single component and, as such can't be modified in different components. A component A having to modify a variable implemented in an other component B need to use one of the operations defined in B, modifying this variable. No cycle is allowed among component dependencies.