Until now, the B language has only supported Boolean and integer basic types, as safety critical railway applications do not need other types. For this purpose coefficients are applied to each data of a B model in order to obtain the desired level of accuracy while retaining the semantics of integer arithmetic on computer (32-bit, non-overflow checking, etc.).
The introduction of support for floating point numbers in the B language was accompanied by the addition of real numbers mathematics, the underlying idea being to be able to specify a treatment with real numbers and to ensure that its floating point implementation is “close” to its specification. The first choice was to fully distinguish real and floating point numbers. Indeed, these two mathematical objects having no or very few properties in common, it seemed more appropriate to have things inconsistent in terms of the B language. The REAL base type, distinct from INTEGER, has overloaded arithmetic operators except the division operator which is specialized (the semantics of the integer division being too specific). The FLOAT type in turn has specific arithmetic operators.
Conversion operators between integers, real and floating point numbers have also been developed to make this extension usable.
Real numbers are mathematical objects having properties close to integer numbers’. Considering INTEGER as a subtype of REAL would have led to so many modifications in the Atelier B theorem prover, hence our decision to create a new basic type REAL, complementing the existing basic types (INTEGER, BOOL and STRING). The immediate consequence of this decision is that an INTEGER value can’t be assigned directly to a REAL variable: conversion fonctions would have to be used instead.
REAL operators having a semantics similar to INTEGER ones, all except the division have been overloaded:
|Greater Than||not supported|
|Lesser Than||not supported|
REAL literals make use of “.” in order to be distinguished from INTEGER literals. For example, 1.0 is the real number mathematically equivalent to the integer 1. The reader may pay attention to the fact that 1.0 is a real literal and not a floating point one. Floating point literals don’t exist as it is not possible to decide syntactly if they can be represented. For ewemple, 1.2 literal can’t be represented as an IEEE floating point literal).
Typing rules for arithmetic predicates and expressions having been redefined as follow:
|Predicate / expression||Conditions|
|x<=y and x>=y||x and y should have the same type (INTEGER or REAL)|
|x+y, x-y, -x, x*y||x and y should have the same type (INTEGER or REAL)|
|x rdiv y||x and y should be element of REAL|
|x ** y||x can be either INTEGER or REAL, y should be INTEGER|
|x mod y, succ(x) et pred(x),||x and y should be element of INTEGER|
|max(E), min(E)||E should be element of POW(INTEGER) or POW(REAL)|
|SIGMA(x).(P|E), PI(x).(P|E)||E should be INTEGER or REAL|
|x..y||x and y should be INTEGER|
Two new well-definedness conditions are added/modified:
|Predicate / expression||Well-definedness condition|
|x rdiv y||y /= 0.0|
|min(x) and max(x)||x : FIN(x)|
Proof Obligation Normalisation
The normalisation of x<y into x+1<=y, that is systematic for INTEGER, is not valid anymore with REAL. Because of this and we do not want to modify proof tools (and have a dramatic impact on all existing B projects), < and > operators are not supported for REAL.
Floating Point Numbers
To be continued.
Impact on tools
Related typing and well-definedness rules (division by zero, access to array elements, etc.) were adapted to the specific language extensions. The proof obligations normalization rules (mathematical lemmas to prove in order to verify B model correctness) must also be suited. Finally the definition of the “B language for implementation” (called B0) has been extended. The distinction between REAL and INTEGER (the property “INTEGER is included in REAL” is false) allows keeping validation rules database untouched. This rules database, and the tools making use of it, that have been validated and certified during industrial developments will not have to be completely redeveloped but simply to be extended without affecting the validity of the existing data.
An Atelier B CASE tool implementing these extensions has been developed and used to validate the proof of concept. It allows generating proof obligations for real and floating point models. The challenge now is to be able to prove the resulting proof obligations. Proof of real numbers can be achieved by extending the rule-based theorem prover of Atelier B. Proof of floating point numbers in turn requires the implementation of other techniques and tools that will be subject to further work. These studies have demonstrated the feasibility of this approach for the modeling phase and the generation of proof obligations. The feasibility of the automation of mathematical proof is needed to assess on its eligibility in the aerospace and automotive worlds.