B Language User Manual

 Versions history

ClearSy : Initial version, 10/03/2009

Chapter « Architectural Clauses » translated by Ramon Brena (ramon.brena@itesm.mx) .

Acknowledgements

This document was originally written by Denis Sabatier (ClearSy).

 

Introduction

The B language and the B method provide a means for developing mathematically proven software and systems, complying with requirements, through the use of rigorous mathematical reasoning. However B doesn’t impose a particular way to perform a development, as well as C++ or ADA do not impose a dedicated method for designing and analysing. Gathering B design patterns and modelling solutions would help any development team to define its own development method. This document aims at providing hints, by examining a number of typical problems and by providing solutions.

To read this document, it is better to have a basic understanding of the B language (abstract machine, refinement, implementation, main mathematical constructs).

Frequently Asked Questions

Inputs / outputs

Implementation / Programming

Modelling / Principes

Proof

Architecture

Concepts And General Advices

In this chapter, some fondamental notions are presented as well as advices for putting into action the B method:

  • mathematical modelling
  • formal specification
  • offensive programming
  • etc.

B Projects

Let start with a general schema of a project making use of B. The B method is composed of :

  • the B language, mathematical and structured notation used to write specification and programs
  • a collection of rules, defining what the proof of a project is.

A typical B project is made of the phases described below.

 

System analysis

This analysis has to be completed before any modelling. It is not possible, as for other kind of project, to start a B project without having a clear understanding of what has to be otianed at the end.

 

Requirements reformulation

Once the problem is well understood, a new formulation of the initial requirements needs to be obtained. The objective is to remove as far as possible ambiguities (we are not yet dealing with mathematical stuff at this stage).

Mathematical modelling

This phase is aimed at producing the B specification of the system. Several methods may be used:

  • « Flat » specification enumeration of the requirements, than allocation to a B structure. The main difficulty is to find a formulation which is compatible with its structuring in B.
  • Specification focusing on the main requirements first. Specification details are introduced with succesive refinements and importations. The main difficulty is to eventually obtain the complete specification while being distributed over several B components.

 

Product design and development

Design and development are backed by proof all along the development cycle. Process ends when all design details have been introduced, leading to a program written in a subset, implementable, of the B language: the B0 language. Atelier B code generators then transform this B0 modelling into compilable source code.

Terminology

  • B project: all the activities using B, starting from requirements and leading to a system complying with these requirements.
  • B development: idem B project
  • B model: a mathematical description which represents some real entities of the target system or of its context. In a B project, several mathematical modellings are used to either represent several aspects of a system, or an aspect at various levels of detail. B models are written down into B components (abstract machines, refeinements), but are independent entities.
  • Abstract Model: idem B model
  • B modelling: activity of creating B models
  • Mathematical modelling: in a B project, idem B modelling
  • System level properties modelling: idem B modelling, while putting the stress on the property-based approach
  • B specification: set of B components and relationships that are equivalent to initial requirements.

Modelling System-Level Properties

Case study

Static and dynamic properties

Modelling static properties

Modelling dynamic properties

MACHINE
    DynamicProperty
ABSTRACT VARIABLES
    fifo, cmd
INVARIANT
   fifo : {T_0, T_MINUS_1, T_MINUS_2} +-> {ON,OFF} ^
   cmd : {ON,OFF}
INITIALISATION
   fifo := {} ||
   cmd := OFF
OPERATIONS
SetCmd(cc) =
    PRE cc : {ON,OFF} THEN
        cmd := cc
    END;

UpdateFifo =
    ANY local_fifo WHERE
        local_fifo : {T_0, T_MINUS_1, T_MINUS_2} +-> {ON,OFF}^
        local_fifo[{T_MINUS_2}] = fifo[{T_MINUS_1}] ^
        local_fifo[{T_MINUS_1}] = fifo[{T_0}] ^
        local_fifo[{T_0}] = cmd
    THEN
        fifo := local_fifo
    END
END

Conclusion

Offensive Programming and the B Method

How To Structure a B Project

What We Have Learned

Architectural clauses

In this chapter we are going to study the architectural clauses used in B. We are going to justify their use, presenting -without being exhaustive- the different decomposition methods used of a B project. Finally, we will recall and justify the usage rules for these architectural clauses.

 

Reminders

1.- The IMPORTS clause allows to create instances of abstract machines, in order to use in the implementation the data and services of these machine instances. When importing an abstract machine, the implementation requires the creation of a concrete instance of this machine, and becomes the father of this instance; only this implementation has the power to modify the instance’s variables, via the modification operations. Thus, the IMPORTS clause allows to an implementation to perform its specification by using the data and services of other programs seen through their specification. So, the decomposition of a problem into subproblems as the factorization of services that can be used by several operations is performed by using the IMPORTS link. This aspect is further developed in the remaining of this chapter.

2.- The INCLUDES clause allows to regroup in an abstract machine the variables, constants and sets -along with their properties- coming from other abstract machines. Thus, the INCLUDES clause is useful for decomposing a complex abstract machine into several simpler abstract machines, simplifying in this way the proving tasks. Indeed, the proof of a component and its « included » machines is globally simpler than the proof of a not decomposed counterpart. The interpretation of « including » is simple: the variables and constants of the included machine become entities in the including machine, and the included operations become usable « specification chunks ». It is possible to include several different instances of a same abstract machine: in this case, the created instances are abstract instances, not accessible by SEES (see later). When a component M includes an abstract machine N, several possibilities could be considered when writing implementation M_imp, which implements the specification of M. The implementation M_imp can import the abstract machine N: in this way, the variables, sets and constants of the included abstract machine in the implementation will be implemented by the variables, sets and constants of the imported instance. The implementation M_imp could as well not import the abstract machine N. In this case, the concrete sets, variables and constants defined in the abstract machine N would have to be defined in the implementation M_imp, either locally, either creating an instance of another component. The choice of this decomposition is taken by the user; the INCLUDES / IMPORTS link combinations is further developed in this chapter.

3.- The SEES clause allows to introduce in a component a list of machine instances, the parts of which (sets, constants and variables) are readable in the component but not modifiable. A component (abstract machine, refinement or implementation) can « see » a machine instance; for doing so, this abstract machine instance would have been previously created using an IMPORTS link elsewhere in the project. This clause could cause a problem known as « aliasing » (see section 4.5.3) if the project is not verified by Atelier B.

4.- The USES clause is actually a specification clause. When a component includes several machines, the included machines could share data (sets, constants and variables) of any included machine by using the USES clause. These data are thus readable but not modifiable. This clause is rarely used.

5.- The PROMOTES clause is not properly an architectural clause, but it allows to an abstract machine (or to an implementation, respectively) to promote operations belonging to included machines (imported, respectively), meaning that the concerned operations become operations in the host machine, that could be externally used.

6.- The EXTENDS clause is defined by the following equivalences:

– In a machine or a refinement: EXTENDS M means INCLUDES M PROMOTES < all M operations >

– In an implementation: EXTENDS M means IMPORTS M PROMOTES < all M operations >

 

Decomposing in B

Before taking care of actual design problems, one of the first problems that should face anyone constructing a specification, after completing the general properties formalization, is the decomposition of the specification. The complete decomposition of a software system is a complex task, involving many different parts. Even if the specifier is able to translate all the components into mathematical formulas, these formulas are just too many to be gathered all in just one abstract machine.

One tempting but bad idea is to cut all the involved formulas into separate chunks, to be kept in independent isolated abstract machines. Indeed, for making the most out of the modeling, at a point it will need to prove some properties derived from gathering all those formulas, meaning that we will have to group the abstract machines in one moment or another. Thus, we loose interest in this kind of simple decomposition. This is exactly what happens if we try to decompose a big specification by means of INCLUDES clauses: in order to implement the specification, we will have to write a grouping machine that includes all of the parts produced by the decomposition. Proving this type of refinement could be a daunting task.

In B, this problem is solved using more abstract specifications. If our complete specification is decomposed in a given number of parts, lets assume that we can measure the complexity of the parts and associate to them a number:

We should find a way to gather those specifications without going beyond a certain complexity level, let us say, Complexity = 15 in our imaginary measuring system. In practice, of course, we will never have such a quantitative measuring system! These figures are useful only to illustrate our point.

We will gather those specifications into groups, each one represented by a more abstract specification, which should not contain all the details in that group. This representation is done implementing (IMPORTS clause) the more abstract specification over the group elements:

The abstract specifications complexity is less than the sum of all the detailed specifications considered because there is not the detail present in the latter. On the opposite, in the more abstract specifications it is possible to prove properties which are consequences of the combined properties of all the represented detailed specifications. This could be generalized to the highest level:

 

INCLUDES / IMPORTS Combination

The INCLUDES link do not allow to structure a project, it allows simply to decompose an abstract machine into several abstract machines. The data of included machines (sets, constants and variables) are grouped in the machine which commanded the inclusion.

When such a decomposition is done, a question that arrives often is how to implement the included entities. We can then use the INCLUDES / IMPORTS method, which is going to be presented in this section.

Lets recall that the fact of including an abstract machine into another abstract machine implies to integrate in the second one all the notions, variables, sets, etc. of the included machine. It is in a way like if we had copied the text defining the included machine inside the including machine, except that we do not have the right to directly modify its variables without touching the operations. This restriction leads us to considering that the included invariant remains true without the need of proving it, because the included machine should prove it elsewhere.

It is possible that the included machine has been implemented elsewhere. When including its specification text into our including machine, we have absolutely not integrated this implementation. How to take advantage of this implementation?

The implementation of the including machine should achieve by itself the data of the included abstract machines and also its own data. To do this, two possibilities are offered to the user:

– The implementation achieves locally that data. Lets take the example of the constants evaluation: actual values are given to abstract sets and concrete constants in the VALUES clause. This is the case of a so-called « explicit » valuation.

(((example boxes follow)))

The example above shows the local valuation of static data. The VALUES clause of the mm_i implementation allows to give an actual value to abstract sets and concrete constants; they are at the same time the abstract sets and constants defined in the mm abstract machine, but also those coming from the included « mi » abstract machine. The accomplishment of dynamic data (variables) follows the same principle.

– The implementation delegates the realization of these data by importing other abstract machines. Lets recall that the variables of a machine can be achieved by linking with the imported variables (liaison invariant or homonymy). Concerning the static part, the VALUES clause allows to give a value to constants and sets. The name of the VALUES clause is followed by a list of valuations. Each valuation allows to give explicitly a value to a constant or set. If some data to be valued has the sam name than a set or constant of an imported machine, then this data cannot be explicitly evaluated; it takes implicitly the value of its homonym data. Otherwise, it should be explicitly evaluated.

 

Combination of IMPORTS /PROMOTES

Frequently, when writing an implementation, the B user identifies new services which should be called in the body of the implementation’s operations. These services, unspecified as operations in the associated abstract machine, and which anyway use (of modify) the same data, cannot be defined in the implementation. Indeed, operations are defined in abstract machines, and it is not possible to define new ones in a refinement or implementation. In fact this corresponds to the need of creating local procedures.

There are two possible cases:

– Either the desired services work over non separable data, case in which these would be truly local procedures, currently not supported in B;

– Either the desired services concern and encapsulate a separated data group; in this case, we could regroup this data in a separated abstract machine, and to use the IMPORTS/PROMOTES combination afterwards.

The IMPORTS/PROMOTES combination consists in regrouping the wanted services with the concerned data in a separated abstract machine, which is imported in the implementation. Very often, some services proposed in the original machine concern only this kind of data. We can then take the handling of these services outside the new machine implementation, and to promote these operations as the implementation of initially proposed services. This is indeed a « top-down » programming technique.

Let us illustrate this technique with an example about inventory control. The inventory is composed by a list of articles which remain undetermined for the moment. The main module should provide the following services:

 

Usage

What We Have Learned

Gluing Invariant

Implicit or Explicit Gluing Invariant

Faulty Invariant When Replacing Variable

Proof Degradation because of a Faulty Gluing Invariant

Detecting Faulty Gluing Invariant

What We Have Learned

Designing Loops With B

Introduction

Designing Loop Invariant

Designing Loop Variant

Different Styles

Variable Scope Resolution in a Loop

What We Have Learned

Developping Basic Machines

Definition

Role of a Basic Machine

Some Examples

Basic Machines Provided With Atelier B

This section needs to be updated, regarding the current basic machines provided with Atelier B 4.0.

Library Machines Provided With Atelier B

This section needs to be updated, regarding the current library machines provided with Atelier B 4.0.

Developping Basic Machines with atelier B

What We Have Learned

Developping Context Machines

Purpose of a Context Machine

Developping a Context Machine

Context Machines within a B project

Asbtract Sets and Typing

What We Have Learned

Algorithms and Numerical Data With B

Introduction to Floating Point Numbers

Decimals

Floating Point Numbers

Precision of B Floating Point Numbers

Precision of the Hardware

Adding Two Floating Point Numbers

Component BASIC_FLOAT

Use of BASIC_FLOAT

Real Numbers in B

What We Have Learned

Sequencing Operations

Implementing Specification

Sequencing Imposed by Specification

Condition-based Sequencing

Sequencing Variables

What We Have Learned

Exponential Growth Of The Number Of Proof obligations: Origins And Solutions

Sequencing COntrol Structures

Too Complicated Algorithmic Refinement

Inappropriate Decomposition

What We Have Learned

Modelling Tables With B

Defining a Table in B0

Initialization

Access

Variable size Tables

Conclusion

What We Have Learned

Implementing Set-based Variables

Introduction

Initialization

Addition or removal of an element

Union, intersection and set-based difference

What We Have Learned

Glossary