B compiler B0 check phase specification

 

Chapter 1 : Introduction

The B compiler allows the anlysis of ASCII source file of a B component. It produces a data structure that represents the component. This data structure is a tree, called Betree 1.
During the construction of this tree, the ASCII source file is analyzed from different point of views:
– Lexical analysis, where the integrity of the lexems in the source is verified.
– Syntaxic analysis, where the conformity of the source with the laguages gramar is verified.
– Semantic analysis, where the identifiers are resolved, and the data is typed by inference.
– B0 Verification, specified in the document, where the implementability (i.e. the respect of the rule that garantee the translation in C, C++, or Ada) of the component is verified.

This document presents the specifications of the B0 verification phase. During this step, two types of operations are carried out:
– Control operations, that verify that the component respect a certain number of implementability rules linked to the clauses.
– B0 construction operations, that facilitate the work of the translation tools.
The B0 verification therefor has a double mission in the B compiler: A policeman mission, that detects a B source conformity label, and a builder mission, that decorates the Betree with B0 types.
This document precisely specifies these two mission, that are carried out in sequence, in the previously stated order.
The rules used to accomplish these missions are exposed and justified in the [REF B] and [SPEC B0C] reference documents. The present document takes up these requirements without justifying them.
The requirements applicable to the B0 verification pass are referenced by an indentifier following the conventions presented in paragraph 2.3.2.
Error messages produced during the semantic analysis phase are implemented by means of the input-output manager of the B compiler, specified un the [CPL4] document.

Chapter 2 : Terminology and conventions used

Terminology

API « Application Program Interface »: Programing interface offered by a library
Library: A library is a set of B components.
B Component: A B component designates indifferently an abstract machine, a raffinement, or an implementation.
Project Dependency graph: The project dependency graph is composed of all the components of the project, a component A is linked to a component B if and only if B is a machine required by A.
Identifier: An identifier designates the whole formed by a B data, meaning its name, its type, and its range.
Machine instanciation: An abstract machine that has formal parameters is instanciated when it is used in a component that gives effective values to the formal parameters.
Required machine: A componant A requires a machine B if and only if A sees, imports, includes, uses, or expands B.
B Module: A B module allows the imitation of an under-system : Its constitutes a part of a B project. A module designates a abstract machine and its succesive raffinements.
Operation: An operation is a service offered by a B module. The operations constitute the dynamic part of a module.
Developped operation: A developped operation is an operation whose body is given in the component.
Project: A project is composed of component that are linked by means of visibility links or importations. The components come from a dedicated development or libraries.
Prototype: The prototype of an operation, also called signature, is composed of the operations name, the list of its input parameters, and the list of its output parameters.
Scalar: Data whose type is an integer, booleen, enumerated set or abstract set element.
Enumerated value: An enumerated value is an element of an enumerated set.

Lexical conventions

This document gives the exhaustive list of the requirement that apply to the B compiler. Each time it is possible, the correspondance with Atelier-B reference documents is furnished. For writing capacity reasons, the following conventions are used:

Format         Example         Source
MTC-xx        MTC-101         Document [MSG TC], message xx
R-xx            R-7.4              Document [REF B], section xx
R-xx-Ryy     R-7.1-R3         Document [REF B], section xx, restriction yy
TC-xx          TC-1.2.9         Document [SPEC TC], section xx
B-xx            B-Header.3     Document [SPEC B0C], exigence xx

Coding conventions

Coding rules

The coding rules are presented in the [DBL2] document will be scrupulously respected.

Coverage of requirements by the source code

The requirements presented in this specification are all marked by an identifier, for example CSYN 1-1 or PROJ 3-8
Each portion of code covering a requirement must explicitly mark this cover by containing a commentary in the following format:

// CTRL Ref : requirement number.

For example, the code that verifies the requirement of CSYN 1-1 must contain the following commentary :

// CTRL Ref : CSYN 1-1

The Makefile must posess an entry check that extracts from the source code the covered requirements (for example by extracting lignes that contain « CTRL Ref : » lexems).
Thus, by typing « make check », we can at any instant verify that the requirements of this specification covered by the B compilers code.

Chapter 3 : Requirements

The figure 3.1 on page 6 presents the general architecture of the B compiler.
The B0 verifier of the B compiler is called after the semantic analysis phase of a component.
[REF B] quote : « The last level of refinement of an abstract machine is named the implantation. It is subjugated to a few additional constraints: For example, it can manipulate only data or substitutions that have a computer equivalent. These constraints make it a computer language similar to an imperative language. »
The goal of the B0 verifier is to make all the controls on the B implantations. In addition, it makes controls on the refinements and specifications. Indeed, these components define data that are meant to be refined in the B developpement cycle. Certain of these data have a type that insn’t refinable by an implementable data. Thus it is possible to warn the user as soon as he writes a specification or a refinement that he is introducing non-translatable data, and so to avoid « bad surprises » during the translation of his project.
Of course, if the goal of the user is to describe a formal specification of a systeme without implementing or translating the associated component, these verifications won’t be usefull. This is why these controls are done in a seperated pass. In addition, thes controls are configurable. The functionnalities of the Ressource Manager, specified in the [CPL5], where used.

Chapter 4 : Syntaxic controls

Introduction

The controls presented in this chapter are syntaxic level controls. They are described and justified in the [CPL3] document, chapter 4, « Syntaxic Controls local to a component » section.
These controls are accomplished by the syntaxic analyser of the B Compiler. They concern:
– Substitutions (paragraph 4.2). The substitutions used in the implementations must not include any undeterminisme. B0 substitutions are called instructions.
– Predicates (paragraph 4.2.1). B0 predicates are called conditions.
– Expressions (paragraph 4.2.1). B0 expressions are called terms.

Controls on substitutions

Principle: The implantation substitutions must be determinist.
The following paragraph gives an exhaustive list of these controls, in addition to the associated ressources. If a ressource is not positionned ou if its value differs from True, then the associated control is carried out, in the case of a problem, the components syntaxic analysis fails.
Ressources prefix: ATB*BCOMP*

Controls on predicates

Principle: The implantation predicates must be conditions. If the ATB*BCOMP*Disable_Predicate_Syntax_Check ressource is positioned on TRUE, then thes controls are not carried out.
– CSYN 7-1 à CSYN 7-8 : prohibited predicates
– CSYN 8-1 à CSYN 8-6 : condition definition
These controls are not configurable.
Exceptions
– ESYNPRE 1 : In the WHILE substitution, the predicate the describes the invariant is not translated. The invariant can therefor be any B predicate: it is not restricted to the conditions.
– ESYNPRE 2 : In the ASSERT substitution, the predicate that describes the condition is not translated. It can therefor be any B predicate: it is not restricted to the conditions.

Controls on expressions

  • Controls

Principle: The implantations expressions must be terms.
The controls that need to be done are described in [CPL3]:
– CSYN 9-1 à CSYN 9-10 : prohibited expressions
– CSYN 10-1 à CSYN 10-4 : definition of the simple terms
– CSYN 11-1 à CSYN 11-4 : definition of the « non simple » terms
– CSYN 12-1 à CSYN 12-7 : definition of the arithmatic expressions
– CSYN 13-1 à CSYN 13-3 : definition of the B0 tables
– CSYN 14-1 à CSYN 14-2 : definition of the B0 intervals
If the ATB*BCOMP*Disable_Expression_Syntax_Check ressource in positioned on TRUE, then these controls are not carried out.

  • Exceptions

– ESYNEXP 1 : In the WHILE substitutions, the expression that describes the variant in not translated. The variant can therefor be any B expression: It is not restricted to terms.
– ESYNEXP 2 : In the CASE substitution, the selection expression must be a simple B0 expression (a simple term).
– ESYNEXP 3 : In the case of a devient_egal substitution, only the following allocations are possible:

- scalar data allocation
- table data allocation
- table element allocation
- boolean data allocation with a B0 predicate (condition)
- B0 record allocation

– ESYNEXP 4 : In the case of a devient_egal substitution, the left member cannot be a list.
– ESYNEXP 5 : In the case of a devient_egal substitution, the right member cannot be a list.
– ESYNEXP 6 : In a B0 operation call substitution, the effective input parameters can be either B0 expressions or litteral caracter strings.

Chapter 5 : Semantic controls specific to B0

Introduction

This Chapter offers precisions on specifique semantic controls, other than the controls relative to the typing of concrete data, that will be studied in the following chapter. These controls concern table compatability that intervene in:
– B0 predicats (conditions)
– B0 substitutions (instructions)
If the ATB*BCOMP*Disable_Array_Compatibility_Check is positioned on TRUE, then these controls are not carried out. Remember that to garantee that concrete tables can be translated, they need to be compatible: They evidently need to have the same type but the need to have recieved syntaxically the same definition domain during their typing. The definition domain of a table is determinated either directly when the table is typed in a typage predicate that explicitly defines the domain, or by inference if the table is typed by means of another table.
In the case of compatibility verification between two concrete tables, different possibilities are destinguished for the typing expressions:
– A constant table : Plage * singleton ;
– A set of total functions : Ensemble_simple –> Ensemble_simple ;
– A set of maplets : -(Terme_simple |–> Terme)} ;
In the first two cases, the definition domains are given directly by the expressions of Plage and Ensemble_simple. The syntaxic verification does not pose a problem.
Concerning the maplet sets, the definition domain need to be « calculated ». The index of a maplet that can only be literal booleans, leteral integers, or enumerated values, the definition domain can be respectivly BOOL, an explicited intervals bordered by the inferior and superior borders of the considered literal integers, or the enumerated set corresping to the considered enumerated values.
The compatibility with other table can be verified from « calculated » definition sets.
It is also necessary to verify that the maplet expressions don’t have « holes », meaning that there exists a total function between the cartesian product of the calculated definition sets and the table arrival set.

B0 predicates (conditions)

– RSEMPRED 1-1 : In the case of an equality or an inequality concerning tables, the tables must be compatible.

B0 substitutions (instructions)

– RSEMSUBST 2-1 : In the case of the allocation of a data table (devient_egal substitution), or in the case of the valuation of constant concrete table, the tables must be compatible.
– RSEMSUBST 2-2 : In a B0 operation call substitution, in the case where an effective input or output parameter is a table, the effective parameter and the formal parameter must be compatible.

Chapter 6 : Semantic controls of typage

Introduction

This chapter specifies the semantic controls relative to the typing of concrete data. These controls are of two types:
– Type control: For each data nature, the exhaustive list of the allowed types are furnished.
– Typing predicate control: Certain data natures can be typed only by certain predicates. The exhaustive list of the typing manners of data is furnished (remember that a data is typed in the first typage predicate that concerns it). If no restriction is furnished, all predicates conform to 4.2.1 are admitted.
Notice: No variable or abstract constants is accepted to type a concrete data, the type of the concrete data being non-translatable.

Terminology

For clarity reasons, the following definitions are recalled:
– Formal scalar parameters: A formal parameter of a machine whose name contains at least one lower case caracter is a formal scalar parameter. It must be typed in the CONSTRAINTS clause of the component. Its type can be scalar or ensemblist. These are called respectively « formal scalar parameter of scalar type » or « formal scalar parameter of ensemblist type ». Example :

MACHINE A(p1, p2)
CONSTRAINTS p1 : INT & p2 <: INT

p1 is a formal scalar parameter of scalar type, whereas p2 is a formal parameter.

– Ensemblist formal parameter: A formal machine parameter whose name contains no lower case caracters is an ensemblist formal parameter. It must not be typed: Indeed, its type is by definition Setof(atype(PARAM)), where PARAM is the name of the parameter.
Example :

MACHINE A(PARAM)

PARAM is an ensemblist formal parameter of type Setof(atype(PARAM)).est un paramètre formel ensembliste de type Setof(atype(PARAM)).

– Term: In this chapter, a term is an expression of the B0 language as defined in R 7-24-2, and not as it is defined in the CPL3 4-7. Meaning that the table expressions and B0 interval expressions are not terms. Notice: The type of a term is of the concrete variable type (cf Typing of a concrete variable)

Types and constraints of data-type table and record

For comprehension reasons, the following points are recalled: – B0 tables: The B0 tables are of P(T1*…*Tn*T0) type, or n¸1 and each type Ti is a basic type outher than the STRING type.
Before defining the notion of the B0 table, the notion of concrete simple set is introduced. A concrete simple set is an abstract or enumerated set, the set of booleans, or a concrete integer interval or a concrete under-set of an abstract set.
Important note: In the case of a simple set defined with an identifier, the identifier must not be an abstract variable or an abstract constant.
A B0 table is a totale function whose starting set is a cartesian product of n concrete simple sets (with n¸1) and whose arrival set is concrete simple set. The n-1 simple sets that constitute the definition domain of the table are also called index sets of the table.
Remember that a table expression is defined by:
– An identifier
– A liste of maplets between brackets
In this context, a maplet is an n-uplet whose index is a simple term restricted to a litteral scalar (litteral integer, literal boolean, or enumerated value of an enumerated set), and the value of any scalar.
-The cartesian product of a plage with a singleton

plage is a simple set
scalar of esemblist type

All the indexs and all the values belong to simple sets.
This condition restricts the possible terms.
– RTYPETAB 1-2 : During an access to a table, the indexs must be of the simple set type.
– RTYPETAB 1-3 : Moreover a table cannot be defined with maplets in the case of an abstract index set. It can only be defined with a slot that have this set as a value.
– RTYPETAB 1-4 : Moreover, the index sets nust not contain in their definition:

- Variables
- Formal, scalar, or ensemblist parameters
- input/output operation parameters

– RTYPETAB 1-5 : The value of a table element must be a term of simple set type.
– The B0 records: The B0 record type is defined by induction. A B0 record type is a type for which each of the fields is of the following types: Z, BOOL, an abstract set, an enumerated set, a B0 table type, or a B0 record type.
The constraints on the B0 record data are defined by induction. Each field of a B0 record must be a concrete data. In particular, if one of the B0 record fields is a record itself, then each field of the later must also be a concrete data.

Typage formal settings scalar machine

These controls are carried out in a B specification.
If the ATB*BCOMP*Disable_Formal_Params_Type_Check ressource is positioned on TRUE, then these controls are not carried out.

Restrictions of type

The types that are authorized for a formal scalar machine parameter are the following:
– If the parameter is of the scalar type:

- RTYPE 1-1-1 : Integer
- RTYPE 1-1-2 : Boolean
- RTYPE 1-1-3 : Abstract or enumerated set element

– If the parameter is of set type:

- RTYPE 1-1-4 : Abstract or enumerated set
- RTYPE 1-1-5 : Abstract set element or integer interval

Restrictions on the typing predicate

Only the following typing predicates are authorized to type a formal scalar machine parameter:

- RTYPE 1-2-1 : Equality predicate with a term.

– Belonging Predicate to one of the following construction:

- RTYPE 1-2-2 : Z, N, N1, NAT, NAT1 ou INT
- RTYPE 1-2-3 : BOOL
- RTYPE 1-2-4 : Explicite B0 interval (CSYN 14-1 or CSYN 14-2) .
- RTYPE 1-2-5 : An identifier representing a formel ensemblist parameter of the machine.

– Inclusion Predicate:

- RTYPE 1-3-1 : Inclusion in a simple set: The simple sets are define in paragraph Types and constraints of the concrete data of types table and record.

Typage formal settings ensemblistes machine

These parameters represent types themselves. No control is necessary.

Typage sets abstract or listed

These parameters represent types themselves. No control is necessary.

Typing a constant concrete

If the ATB*BCOMP*Disable_Concrete_Constants_Type_Check ressource is positioned on TRUE, then these controls are not carried out.

Type restrictions

The types authorized to type a concrete constant are the following:

- RTYPE 2-1-1 : Integer
- RTYPE 2-1-2 : Boolean
- RTYPE 2-1-3 : Abstract or enumerated set element
- RTYPE 2-1-4 : Abstract set element or integer interval
- RTYPE 2-1-5 : B0 table
- RTYPE 2-1-6 : B0 record

Restrictions on predicate typing

Only the following described typing predicates are authorize to type a concrete constant: – Belongging predicate:

- RTYPE 2-2-1 : Belonging to a simple set: The simple sets are defined in paragraph Types and requirements of concrete data of types table and record
- RTYPE 2-2-2 : Belonging to a set of total functions. A the index sets and arival sets must be simple sets (This type of predicate allows the defining of a table)
- RTYPE 2-2-3 : Belonging to a simple term extension set.
- RTYPE 2-2-4 : Belonging to a record set.

– Equality predicate:

- RTYPE 2-3-1 : Equality with a term.
- RTYPE 2-3-2 : Equality with a B0 table.
- RTYPE 2-3-3 : Equality with a B0 interval.
- RTYPE 2-3-4 : Equality with a B0 integer set.
- RTYPE 2-3-5 : Equality with a B0 record in extension.

– Inclusion predicate:

- RTYPE 2-4-1 : Inclusion in a simple set: Simple sets are defined in the paragraph Types an requirement of concrete data of types table or record.

Typing a variable concrete

If the ATB*BCOMP*Disable_Concrete_Variables_Type_Check ressource is positioned on TRUE, then these controls are not carried out.

Type restriction

The authorized type to type a concrete variable are the following:

- RTYPE 3-1-1 : Integer
- RTYPE 3-1-2 : Boolean
- RTYPE 3-1-3 : Abstract or enumerated set element
- RTYPE 3-1-4 : B0 table
- RTYPE 3-1-5 : B0 record

Restrictions on predicate typing

Only the following described typage predicates are authorized to type a concrete variable: – Belonging predicate:

- RTYPE 3-2-1 : Belonging to a simple set: The simple sets a redefined in the paragraph Types and requirement of concrete data of type table and record.
- RTYPE 3-2-2 : Belonging to a set of total functions. All the index sets and arrival sets must be simple sets. (This type of predicate allows the definition of a table).
- RTYPE 3-2-3 : Belonging to a set in extension of simple terms.
- RTYPE 3-2-4 : Belonging to a set of records.

– Equality predicate:

- RTYPE 3-3-1 : Equality with a term.

Typing an input parameter of operation

If the ATB*BCOMP*Disable_Operation_Input_Parameters_Type_Check ressource is positioned on TRUE, then these controls are not carried out.

Restrictions type

The types authorized to type input operation parameters are the following:

- RTYPE 4-1-1 : Integer
- RTYPE 4-1-2 : Boolean
- RTYPE 4-1-3 : Abstract or enumerated set element
- RTYPE 4-1-4 : B0 table
- RTYPE 4-1-5 : B0 record
- RTYPE 4-1-6 : Caracter string

Restrictions on predicate typing

Only the following described typage predicates are authorized to type an operation input parameter: – Belonging predicate:

- RTYPE 4-2-1 : Belonging to a simple set: The simple sets a redefined in the paragraph Types and requirement of concrete data of type table and record.
- RTYPE 4-2-2 : Belonging to a set of total functions. All the index sets and arrival sets must be simple sets. (This type of predicate allows the definition of a table).
- RTYPE 4-2-3 : Belonging to a set in extension of simple terms.
- RTYPE 4-2-4 : Belonging to a set of records.
- RTYPE 4-2-5 : Belonging to the STRING set

– Equality predicate:

- RTYPE 4-3-1 : Equality with a term.

Typing an output parameter of operation and a local variable

If the ATB*BCOMP*Disable_Operation_Output_Parameters_Type_Check ressource is positioned on TRUE, then the controls relative to the operation output parameter are not carried out. If the ATB*BCOMP*Disable_Locale_Variables_Type_Check ressource is positioned on TRUE, then the controls relative to the local variables are not carried out.

Type restrictions

The types authorized to type a operation output parameters or a local variable are the following:

- RTYPE 5-1-1 : Integer
- RTYPE 5-1-2 : Boolean
- RTYPE 5-1-3 : Abstract or enumerated set element
- RTYPE 5-1-4 : B0 table
- RTYPE 5-1-5 : B0 record

Restrictions on predicate typing

The operation output parameters and the local variables are not typed by a typing predicate but by their use in substitutions. There are therefor no control to be be carried out.

Chapter 7 : Controls semantic of valuation, instantiation, and initialization

Introduction

Appart from the verifications concerning their typing, a certain number of data is submitted to semantic controls during the B0 verification phase. These controls goal is to verify that the values given to these data is translatable by the Atelier B translators.
The concerned data are:
– Concrete variables. In a B0 implementation, the INITIALISATION clause allows the initialization of these concrete variables. The 7.2 paragraph give the controls to be carried out.
– The machines formal parameters. The use of a machine posessing formal parameters in a B0 implementation implicates the instanciation of these parameters in the IMPORTS and/or EXTENDS clauses. The paragraph 7.3 explicits the associated controls.
– Concrete constants. A B0 implementation must furnish a value to each of its concrete constants: it is the concrete constant valuation step. The paragraph 7.4 give the controls to be carried out during this phase.
– Abstract sets. A B0 implementation must furnish a value to each of his abstract sets: it is the abstract set valuation step. The paragraph 7.5 give the controls to be carried out during this phase.

Controls on the initialization of variables concrete and local variables

If the ATB*BCOMP*Disable_Variables_Initialisation_Check ressource is positioned on TRUE, then thes controls are not carried out.
RINIT 1-1 : The right part of an initialization (instruction) must have only initialized variables.
The « different paths » of the B0 code (case of instruction branches if and case) are managed. Meaning, for example, that a variable that is not initialized in all the branches of a case, and that is not initialized in the « default case » part, is considered as non initialized in the case output.
Moreover, in the case of the operation call instruction, the effective input parameter must be initialized.
Finally, in the case of the while instruction, the body must be controled, but the newly initialized variables must be considered as non initialized in the while output. Indeed, passing at least once in the loop is not assured.
Example :

IF (condition)
THEN
-
X := 2
Y := X <----- initialisation valide
}
ELSE
-
Y := X <----- initialisation non valide car X n'est pas initialisée
}

Controls on the instantiation of params formal machine in terms IMPORTS & EXTENDS in implementation

If the ATB*BCOMP*Disable_Parameter_Instanciation_Check is positioned on TRUE, the these controls are not carried out.
The instanciation of a Mimp machines formal parameter takes place in the IMPORTS or EXTENDS clause of the component M that imports or extend in Mimp. In this clause, the formal Mimp parameter f1 : : : fn are instanciated with the e1 : : : en effective parameters.
e1 : : : en must respect the rules of formal parameter instanciation. These rules are exposed in paragraphs 7.3.1 and 7.3.2

Controls on the valuation of constant concrete and abstract sets

If the ATB*BCOMP*Disable_Valuation_Check ressource is positioned on TRUE, thes controls are not carried out. The valuation of concrete constants is submitted to semantic control:
RVAL 0-1 : All concrete constants must be valuated. Each concrete constant must be valuated in the VALUES clauses once maximum. Once and only once if the concrete constant is not homonym to same nature data of a seen or imported machine instance, 0 times otherwise (The data is implicitly valued).
RVAL 0-2 : The right part of a valuation must already be valued.
– The paragraph 7.4.1 explicits the RVAL 1-x concrete scalar constant valuation requirements. scalaires.
– The paragraph 7.4.2 explicits the RVAL 2-x concrete table type constant valuation requirements. scalaires.
– The paragraph 7.4.3 explicits the RVAL 3-x concrete interval type constant valuation requirements.

Controls on the valuation of abstract sets

The valuation of abstract sets is submitted to semantic controls: RVAL 4-1 : All abstract sets must be valuated.
Each abstract set must be valuated in the VALUES clauses once maximum. Once and only once if the abstract set is not homonym to same nature data of a seen or imported machine instance, 0 times otherwise (The data is implicitly valued).
The only possible valuations for an abstract set are:
– RVAL 5-1 : An abstract set or a constant interval of a reuired machine – RVAL 5-2 : An intiger interval, included in INT, non empty.

Chapter 8 : B types construction

Introduction

In order to facilitate the work of the translation tools, construction operations of B0 type are used. A pass is made on all B0 language indentifiers (destined to be implemented) in order to construct for them a auxilary type in a formalism closer to programing language types (C, C++, ADA). This type construction step is the last step of the B0 verifictation phase.Their must therefor be no B0 type construction impossibility case (The necessary controls have been carried out beforehand).
The goal of this cahpter is to specify the passage from a B type to a B0 type. In order to do that:
– Paragraph 8.2 will expose the modeling of B0 types (B type modeling is described in [CPL3])
– Paragraph 8.3 will explicit general order proprieties that need to be verified by the types
– Paragraph 8.4 will take each B type and specify its associated B0 type construction.

Modeling types B0 through classes

The T_B0_type factorises the proprieties common to B0 types. The following classes, that inherit of T_B0_type, define « terminaux » types:

- T_B0_base_type, that modelises basic types (meaning basic programing language types: INT, BOOL...). The modelised type can be bordered (the borders are referenced). A field represents the predefined B base type, T_builtin_type instance.

Moreover, in the case of data belonging to an interval, this interval is referenced.

- T_B0_abstract_type, that modelises an abstract set element type. The set is referenced as is its valuation.
- T_B0_enumerated_type, that modelises an enumerated set element type, or an enumerated ser type. The enumerated set is referenced as are its different values.
- T_B0_interval_type, that modelises an interval type. The borders are referenced.

Moreover, in the case of an under-set of an abstract set, the abstract set is referenced as is the name of the under-set.

- T_B0_array_type, that modelises a table type. The B0 types of the source type and destination are referended, as is a unique name allocated during the creation and used during the translation.
- T_B0_label_type, that modelises a record field. The label name is referenced, as is its type.
- T_B0_record_type, that modelises a record type. The B0 types of the fields are references (through a list of T_B0_label_type instances), as is a unique name allocated during the creation and used during the translation.

General on the construction of types B0

– The B0 verification phase must, for each B0 source identifier, build an auxilary type in a fomalism closer to a programing language type. – An instance of a built B0 type must reference the dual B type instance from which it was built. – And vice versa, a B type instance used to build a B0 type instance must reference it.

B0 types constructions

In this chapter, for a given identifier, each B type is taken up and the transformation to its B0 type is specified.

Basic types (T base type)

– T_predefined_type :
A T_B0_base_type is created.
The 8.2 figure page 29 presents the construction of B0 type of a T_predefined_type type data.
The borders of the T_predefined_type instance allows the informing of the T_B0_base_type instance borders.
The value of the field representing a predifined B base type informs the similar T_B0_base_type field.
Moreover, in the case of a data belonging to an interval, this interval is referenced from the value of the field corresponding of T_B0_base_type.

– T_abstract_type :
This case corresponds to the typing of an abstract set element E (of setof(atype(E)) type).
An instance of T_B0_abstract_type is created.
The 8.3 figure on page 30 presents the construction of the B0 type of a T_abstract_type type data. The B0 type of the element to type is the B0 type of atype(E) that is built during the E identifier typing analysis (cf paragraph 8.4.2 in the case of the transformation of an instance of T_setof_type class).
If this last B0 type has not yet been built, the T_B0_abstract_type instance is still built, but the fields corresponding to the abstract set valuation is set to « null ».

– T_enumerated_type :
This case corresponds to the typing of an enumerated set element E (of setof(etype(E)) type).
An instance of T_B0_enumerated_type is created.
The 8.4 figure on page 31 presents the construction of the B0 type of a T_enumerated_type data.

The field corresponding to the name of the enumerated set (T_ident instance) is informed from the similar field of the T_enumerated_type instance.
Moreover, the list of the enumerated values is informed from the corresponding list of the T_ident instance representing the enumerated set.

Types constructors (T constructor type)

– T_set_of_type :
This case corresponds to the typing of a setof(X) type data, where X is the type before valuation. The built B0 type depend on the value of X.

– X a T_product_type instance:
A T_B0_array_type instance is created.
The 8.5 figure on page 32 presents the construction of the B0 type of a T_setof_type(T_product_type) type data.
(The type control of the B0 phase garantees that we are in presence of a table and that the n different types intervening in the cartesian product are implementable). The B0 types corresponding to the (n-1) first elements of the cartesian product are built and listed between them, and inform the field corresponding to table source type. The n-th element of the cartesian product is built, and informs the field corresponding to the table destination type.

– X is not an instance of a basic type:
This type does not correspond to an implementable type. The B0 verification phase, concerning type controls, assures that this case is not possible.

– X is an instance of T_abstract_type :
An instance of T_B0_interval_type is created.
The 8.6 figure on page 33 presents the construction of a B0 type of a T_setof_type(T_abstract_type0 type data. We are in the case of an under-set of an abstract set. The corresponding B0 abstract set needs to be built. Remember that an abstract set can be valuated either with another abstract set or with an interval of integers. The B0 abstract set, instance of T_B0_abstract_type, must reference the valuation abstract set or the valuation (B0) interval.
The B0 abstract set thus created, and the X identifier defining the under-set then reference the fields corresponding to the created B0 interval.
Finaly, the borders of the T_abstract_type instance X allowing to inform the borders of the created T_B0_interval_type instance. Warning: The identifier valuation step (abstract sets and concrete constants) must be taken into consideration and the borders must be referenced after diving.

– X is an instance of T_enumerated_type :
An instance of T_B0_enumerated_type is created.
T_setof_type(T_enumerated_type).
The field refering the enumerated set is informed from a similar field of the T_enumerated_type instance.
Moreover, the list of the enumerated values is informed from the corresponding list of the T_ident instance representing the enumerated set.

– X is an instance of T_predefined_type :
An instance of T_B0_interval_type is created.
The 8.8 figure of page 35 presents the construction of the B0 type of a T_setof_type(T_predefined_type) type data. The borders of the T_predifined_type allowing the informing of borders of the created T_B0_interval_type instance.

– T_product_type :
This type does not correspond to an implementable type. The B0 verification phase, concerning type controls, assures that this case is not possible.

– T_record_type :
A T_B0_record_type instance is created.
The 8.9 figure on page 36 present the construction of a B0 type of a T_record_type type data.
Remember that a T_record_type instance references the list of the T_label_type instances that constitute it. The corresponding T_B0_label_type instance list must be built. The created T_B0_record_type instance creates a reference on this list.

Others types

– T_generic_type :
This case cannot be encountered, because T_generic_type is not a type use to type an identifier. Only f g and [ ] have types that are T_generic_type instances.

– T_label_type :
An instance of T_B0_label_type is created.
The 8.9 figure on page 36 presents the construction of the B0 type of T_label_type type data. Remember that an instance of T_label_type has a field corresponding the label identifier, and a field corresponding to the label type. The corresponding B0 type of this last type must be built. The created instance of T_B0_label_type then references the label identifier, and its B0 type.