Architectural Clauses

Introduction
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
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.
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.
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” if the project is not verified by Atelier B.
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.
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.
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.
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.
Using B - Previous
Concepts
Next - B Examples
Fuel Level
Last modified 3mo ago
Copy link
Contents
Introduction
Reminders
Decomposing in B
INCLUDES / IMPORTS Combination
Combination of IMPORTS /PROMOTES