Real and floating point numbers

 Introduction

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.

Language Extensions

Real Numbers

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.

 

Operators

REAL operators having a semantics similar to INTEGER ones, all except the division have been overloaded:

Addition +
Substraction
Multiplication *
Division rdiv
Greater Than not supported
Greater Equal >=
Lesser Than not supported
Lesser Equal <=

Literals

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

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

Well-definedness

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.

 

Perspectives

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.