B compiler general design

Note : this translation of the original .pdf documentation don’t include any pictures. If you want to see them, refers to .pdf documentation.

 

Chapter 1 : Introduction

Object

This conception document describes the technical solutions that have been chosen in order to satisfy functions and constraints presented in the specification documents [CPL6] & [CPL8]. The key elements of these documents are recalled in paragraph 1.3 and 1.4 .
The conception presents this software in the following aspects :
– Static aspect : Decomposition into main constituents, identification data exchanged between these components and with the outside.
– Dynamic aspect : Sequencing of operations carried out by the software.
– Implantation on target hardware.

Layout

This document specifies the design choices of modules which form the core of the B compiler, that is :

  • Analyzers

– Lexical (part I)
– Syntaxic (LR, part III and high level, part II)
– Semantic (part IV).

  • Managers (part VI)

– for Objects
– for BeTree
– for Metaclasses
– for Clocks
– for Projects

 

The annexes displays some precious informations for the reader who would like maintain or upgrade the B Compiler :
– The A annexe gives the correspondence between source files of the compiler and their functionalities.
– The B annexe gives the correspondence between functionality of the sources compiler, the compiler, and the associated source files.
– The C annexe gives the method to follow in order to add a class into the Betree.
– The D annexe gives the method to follow in order to enrich the B langage reconized by the compiler

Reminders’s functional

Lexical analysers

The Lexical analyzers mission is specified in the [CPL6] document. It consists in creating a lexemes flow, modeled with the T_lexem class, representing the analyzed B component’s lexemes.

The B source files can now contain the text of many components. Such a file is called « fichier multi-composants ».

So far, the atomic unit managed by the compiler B is a B source file, the lexical analyzer analyzes’ all present components in a « multi-composants » (multi-component) file, and creates a stack flow of lexemes.

Syntactic analyzer

Syntactic analyzers mission is specified in the [CPL6] document: – A syntaxic high-level analyzer, procedural and recursive, is responsible for analyzing substitutions & component anatomy
– A LR analyzer is in charge of analyzing formulas (expressions & predicates).

The high-level analyzer manages the semantic analysis. In particular :
– It calls the LR Analyzer.
– It must resynchronize the analysis in the event of an error, in order to implement a return error mechanism.

Semantic analysers

The Semantic analyzers mission is specified into the [CPL8] document. It consists in executing the following operations :
– Create or load, from a disk, The BeTrees of required components.
– Make semantic controls on components (transversality of SEES, . . . ).
– Make anti-collision controls.
– Resolve identifiers.
– Data typing. Verify the types compatibility in the expressions & substitutions.

Functional constraints

General constraints

The compilers core must obey to the followings functional constraints :
– Production of accurate (Errors are located by the {file name, line number, g colonn number} triplet) and detailed error messages.
– Construction of a BeTree that acurately represents the analyzed B components, in conformity to requirements contained in documents [CPL6] et [CPL8].

The  » multi-composant « (multi-component) mode must be supported natively, i.e. the result of the creation of n BeTree components in a file must be identical to the results given by the union of the creation of n Betree units obtained by storing each of the n components in a file of its own.
– Compliance with programming rules specified in [CPL2].

No common mode

The compiler core must not have any common mode with the first string of transcoding in Atelier B. In order to accomplish this, the followings constraints must be respected :

  • Software resources

The compiler core can’t use the followings software resources :
– Pre-processor C and bpp
– Parseurs B, C et K
– Type Checker, B0 Checker
In order to respect this constraint, the compiler core will not use any software resources external to the development environment of the B Compiler.

  • Language and programming environment

The compiler core can’t be write in Language C, and can’t be developed with the compilation/edition string of the Sun links delivered with Solaris IDE.

In order to respect this constraint, the core will be writen in C++ with the environnement of compialtion/edition of links Gnu gcc ».

Chapter 2 : Terminology and conventions used

Terminology

API « Application Program Interface » –> Application Programing Interface offered by a librairy.

Clock –> Value obtain from a clock manager. The manager gives the possibility to change the hour, or to request the current hour. Clocks are used in algorithm to mark the different phases of a loop : if 2 elements have the same clock, they were created in the same phase.

Conventions and syntax

– The « objets informatiques »(computer objects) like file names, windows or applications choice in menus are write in a non-conventional font, as shozn in the following example.

  La machine MM.mch.

– Input/Output exchanges between the user and the software are described with the same font. In order to differenciate the Inputs and Outputs, messages produced by the software are preceded by the symbol >, and inputs by the symbol %, like in the following example :

  % ls
  > AA.mch AA_1.imp SCCS

Chapter 3 : Description’s and analysis’s ressources

Hardware’s resources

The B Compiler is available on same systems as Atelier B. Moreover, it must be conform to ANSI-C++ and POSIX standards, in order to facilitate its portability to other environments.

Software’s resources

The compiler core does not use any resource files external to B Compiler, except the standard POSIX librairy.
Reminder: Paragraph 1.4.2 on page 3 specifies constraints of the no-common mode on the compiler core. Internal software resources of B Compiler used by the compiler core are the followings :
– Traces manager, specified in the [CPL4] document.
– Memory manager, specified in the [CPL3] document.
– BeTree manager, specified in the [CPL7] document.
– Input/Output manager, specified in the [CPL5] document.

First part : Lexical analyzer

Chapter 4 : Static structure

External Interfaces

Lexical analysis of a source file

  • Prototype
   void function lex_analysis(
   const char *file_name_acp,
   const char *second_file_name_acp = NULL) ;
  • Description

The function « lex_analysis » makes the lexical analysis of a b source file, the name of the file is given by the parameter « file_name_acp ». The parameter « second_file_name_acp » is optional. It gives the possibility to submit an alternate name of a file to load. It is used in the following context : a B component refines an A component. We don’t really know if A is a specification or a refinement. The B language doesn’t give us any information on this subject. So, we call « lex_analysis » with :

  - file_name_acp = A.ref
  - second_file_name_acp = A.mch

In the event of an error of the lexical analyzer, an appropriate error message is made, and the function « lex_analysis  » returns NULL.

  • Searching path

The loaded file is searched for sequentially :

  1. In the current folder
  2. In the eventual search directorates of sources files, provided throught the function
 "add_source_path", described in paragraph 4.1.2, and in the order they were added
("first added, first used").
  3. In the source files list, specified by the .db file of the Atelier B project provided	
 by the means of the "load_project_database" function, described in paragraph 4.1.3.
  • Note : If the function « set_file_fetch_mode(FFMODE_MS) » was called, then only the list of specified files by Atelier B is used.

Search directory’s add for source files

  • Prototype
   void function add_source_path(const char *new_source_path) ;
  • Description

The function « add_source_path » adds a search path for B source files. It is used to specify the path that gives the localization of source files from a library. The search path is added at the end of the list of the search paths already entered. Search paths are modeled with the class T_path, which export following methods :
– Obtaining the path name :

   const char *function get_path_name(void) ;

– Obtaining the path length :

   size_t function get_path_len(void) ;

– Obtaining the next path :

   T_path *function get_next(void) ;

The following function allows access to search path list :

   extern T_path *function get_source_paths(void) ;

Taking into account the database project

  • Prototype
   void function load_project_database(const char *database_file_name) ;
  • Description

The function « load_project_database » allows to request that a project database be taken into account. Functions for project management are described in chapter 21.

Chapter 5 : Dynamic analysis

Search source file’s

Prototype

   FILE *function open_source_file(
   const char *file_name_acp,
   size_t &path_len,
   size_t &file_size)

Description

The « open_source_file » functions goal is to load the B component named « file_name_acp » by following the algorithm presented at paragraph 4.1.1. It returns NULL if the file was not found, or else a file descriptor. In this case, parameters « path_len » and « file_size » are upgrade respectivly :
– Length in number of character in the directory that contains the file.
– The size of the file in bytes.

Algorithm

There are 2 searching algorithms depending on the use of the B Compiler: online use, or use with projects managed by Atelier B.

  • Online use

The different searching paths are examined sequentially. Directly given path by « add_source_path » are obtained by means of « get_source_paths », and project databases paths by means of « get_database_paths ».
For each path, we build the string « acces path/file_name_acp », and we see if the file exists by using the POSIX « stat » function, which returns in addition the file size.
If so, the file is opened with « fopen », and the function returns the specified informations.
If not, the search continues.

  • Use with projects managed by Atelier B

Different projects are examined sequentially. Directly given projects by « load_project_database » are obtain by means of « get_libraries » (Cf 21).
For each project, we search the the file (without its suffix) by means of the function « search_component », that returns the component descriptor.
The file access path is recovered in the project descriptor with the « get_decomp_dir » method.

Loading memory file

The file is loaded in memory in the « lex_analysis » function. The global table « load_sct » is allocated to the necessary size, then filled with all the characters of the file that are read through the function « getc ».
The loading of the file into memory gives more flexibility to the Lexical analyzer, who can reverse changes, if needed, when running an analyze.
A FIFO of memorization of positions is allocated to allow to the Lexical analyzer to keep a history of positions(line, column) which it analyzed. Particularity of this stack : a « push » into a full stack is possible, but provokes deletion of the oldest element of the stack.

Characters are obtained by successive calls to the function « next_car », who returns the next character in the lexeme flow. On this occasion, indicator of current position (line, column) in the file is updated depending on the character that has been obtained.
This couple is then stacked in FIFO « lifo_pos_sop ».

Function « prev_car » allows to reverse changes in the lexeme flow. It reverses cahnges in « load_sct », and restores the associated position from the FIFO « lifo_pos_sop », thus avoiding calculations of previous positions, who would not necessarily be feasible because the BeTree doesn’t model tabulations, backspaces, and carriage returns.

Calculation of lexemes

Prototype

   static void function get_lexems(void)

Description

This function calculates all lexemes of source files stocked in the « global lex_sct » table. For each file component, results are then transfered into lexemes stack flow « first_lex_stack/last_lex_stack ».

Algorithm

The function sequentially runs throught the file, isolating character groups. For each iterations, The following work is done:
– Jump the obsolete « blancs ». By « blancs », we mean backspaces, tabs, return cabs (format Dos or Unix).
– If end of file is reached, finish analyze.
– If not, in case of comment beginning, analyze this comment (function description in paragraph 5.4.4).
– If not, in case of word beginning, analyze word. (function description at paragraph 5.4.5)
– If not, in case of number beginning, analyze number.
– If not, look for a language terminal. (function description at paragraph 5.4.6)
– If not, produce an error message.

Each time a lexeme is recognize, the function creates an instance of the appropriate T_lexem class. The class constructor will also string automatically this instance in the queue of the already created lexeme flow.

Analysis of a comment

 

  • Context

If lexical analyzer detect the character ‘/’, then it’s a potential beginning of a comment.
It advances to the next character. If it’s a ‘*’, then it is indeed a comment, and the function « analyse_comment » is called.
If not, it’s not a comment : lexical analyzer returns to the ‘/’ with the « prev_car » function.

  • Algorithm

If the first character is a ‘?’, the comment can be translated.
Characters are read one by one until we find the sequence ‘*/’ or ‘?*/’ in the case of a translatable comment.
Remember comments are modeled by lexeme types L_COMMENT or L_KEEP_COMMENT, and that by default they are invisible to the syntactic analyzer.

Analysis of an Identificator

 

  • Context

If lexical analyzer detects a lettre, then the « analyse_word » function is called.

  • Algorithm

– As long as we are on a letter, a number, a ‘.’ or a `_`, then the process continues.
– Specific case : if we have a `.` : the process must continue only if the `.` is followed by an identifier. A necessary & sufficient condition for this is that the item that follows the `.` is a letter.
If not, we stop before the `.` and it will be transformed into « L_DOT » when the next lexeme is analyzed. – The « dot_found » boolean is set to TRUE (it’s a local variable initiated at FALSE in beginning loop).
– If not, The words last letter is reached. We look if the obtain word is a key word (this test is not made if the identifier includes a point). To accomplish this, the secondary « lookup_builtin » function is called and returns the corresponding lexeme if a key word is found.
In this case, the lexeme is returned. If not, a lexeme of « L_IDENT » or « L_RENAMED_IDENT » type is created, depending on the value of the boolean « dot_found ».

Line pointers update

Prototype

   void function compute_lines(void)

Algorithm

During this step, we update pointers in the beginning and end of lines, as well as the following and preceding lines. The figure 5.2 illustrates the topology of the lexeme flow that needs to be produced.
For this, the lexeme flow is scanned sequentially and are continually memorised lexemes that describe :
– The beginning, of the previous line
– The beginning of the current line
– The beginning of the next line
In order to do this, the function runs line by line, searching for each line beginning and the beginning of the next line. Then, for all lexemes of the line, pointers « prev_line », « next_line » and « start_of_line » are updated.

Definitions expansion

The definition expansion is done by 4 successive steps :
1. Syntactic analyze of the definitions.
2. Obtaining the order of dependence of the definitions.
3. Expansion of the definitions into definitions.
4. Expansion of definitions into the source file.

The figure 5.3 show the 3 first steps of this function.

Syntaxic analysis of definitions

 

  • Prototype
   void function parse_DEFINITIONS(void)
  • Main algorithm

We run through the lexeme flow until L_DEFINITIONS is found :
1. We verify that this is the first occurrence of this lexeme. If that is not the case, there are more than one occurrence of the clause : we produce an error message.
2. While we are in the DEFINITIONS clause, we analyze definitions one by one, as following :
– We retrieve the definition name, and we verify that the name is not already used with the secondary « find_definition » function.

 - If the name of the definition is an identifier, we create the associated instance of T_definition

 - If not, and if the name of the definition is a definition filename (syntax "fic"

or <fic>), then we make a lexical analysis of this file into a temporary lexeme flow. this analyze happens by recursively calling the lexical analyzer on the considered file. The lexeme flow obtain is inserted into the lexeme flow currently analyzed, instead of the file name, and the syntactic analyze continues its analyze from there.

 - If not, there is an error

– If the current lexeme is a L_SCOL, we continue the definitions analyze. If not, the DEFINITIONS clause is finished.
3. We divert the machines lexical flow in order to make the DEFINITIONS clause lexemes disapear.

  • Syntaxic analysis algorithm of definition

1. We retrieve the definition name
2. If current lexeme is L_OPEN_PAREN, we retrieve the formal parameters of the definition, which must be two by two distinct identifiers, separated by commas. For each formal parameter, one T_ident instance of ITYPE_DEFINITION_PARAM type is created.
3. We call the « find_end_of_def » private method that returns the end of the definition. If the definition is empty, then the returned item is there « == » on which we were located prior to the call. Then we update the « first_rewrite_rule » and « end_rewrite_rule » fields.

Obtaining the order of definition dependencies

 

  • Prototype
   void function order_DEFINITIONS(void)
  • Algorithm

The algorithm uses the « usr1 », « usr2 » and « tmp » fields inherited from T_object : if f is a definition, then the fields are used as follows : – usr1 : number of incoming arrows, i.e. f->usr1 = number of arrows that come in f (g has only one inbound arrow in f if g use f)
– usr2 : last incoming arrow, i.e. f->usr2 = g if, and only if, g is the last to set an incoming arrow in f
– tmp : order counter
We use a classic level numbering algorithm. In each step n, we calculate the number of arrows inbound in each definitions.
Definitions that don’t have inbound arrows are sources, and can be withdrawn from the processes They will be part of level n definitions (information stocked in the « tmp » field).
If no source is found when running a given step, there is a circular dependencies between definitions that can be traced through the usr2 fields of increminated definitions.

Expansion of definitions into definitions

   void function expand_DEFINITIONS_in_definitions(void) ;

This function calls the « expand_def » function described in paragraph 5.6.5, assigning the definition lexeme flow as a parameter.

Expansion of definitions into source file

   void function expand_DEFINITIONS_in_source(void) ;

This function call the « expand_def » function described in paragraph 5.6.5, assigning the component lexeme flow as a parameter.

Secondary expansion function of definitions into a flow of lexemes

 

  • Prototype
   static void function expand_def(
   T_lexem **adr_first_lexem,
   T_lexem **adr_last_lexem)
  • Algorithm

– Set « expand_state » to TRUE

– While « expand_state » is TRUE :
1. Set « expand_state » to FALSE. It will be set to TRUE only if we actually expand a definition. This loop allows us to expand definitions that contain definitions
2. Run through the lexeme flow.
3. For each flow identifier, we look and see if it has the same name as a definition.

 If true :
 - If the definition has formal parameters, we verify that this identifier is

followed by the appropriate number of effective parameters.

 - We clone the right side of the rewriting rules. When cloning, formal parameters

are replaced by effective parameters.

 - We divert the original lexeme flow in order to replace definition calling by

its expansion, as illustrated in picture 5.4

 - Set "expand_state" to TRUE

Secondary search function of the end of a definition

 

  • Prototype
   T_lexem *function find_end_of_def(T_lexem *first)

The parameter « first » must be pointed on the == lexeme of the definition of which we are searching for the end. The return value is the last lexeme of the definition if it’s not empty, the == if it is empty. If there is an error, the function prints a message & stops the execution.

  • Algorithm

1. Advance to next lexeme. 2. We run through the lexeme flow until we are beyond the end of the definition. We have exceed the end of the definition if :
(a) the end of the lexeme flow is reached
(b) We are on a clause name (other than END )
(c) We are on a ==
(d) We are on a definition file name
3. Then we go through the lexeme flow in reverse, the depending on the item on which we stopped : (a) flow end: if there is no errors, the next lexeme is a END. In this case, the last lexeme of the definition is the lexeme preceding END.
(b) a clause: If it’s a component beginning clause, the previous lexeme must be a END, and in this case the last lexeme of the definition is the lexeme preceding this END. If not, the last lexeme of the definition is the lexeme preceding the clause name.
(c) a == or a definition file name : We go back through the lexeme flow to find a semicolon (;) or fall back on the == of the definition (ie the lexeme that became a parameter of the function) If we find a semicolon, the last lexeme of the definition is the lexeme preceding this semicolon If not (we’re back to the beginning point), we print an error message and we stop the execution.

Checksums calculation

Checksums are calculated from the encryption algorithm MD5. This algorithm from the public domain is used in systems of security encryption « RSA Data Security », PGP, and intensively used in computer applications security It allows us to obtain a string of 128 bits representing a binary sequence in a « unique » way. Its specifically described in this document (Reference : RFC 1321).
The probability for 2 different sequences to have the same checksum is 1/2^64 .
Checksums of a clause are obtained by providing to algorithm MD5 the names of the lexèmes composing the clause, ignoring lexemes of comment type.

  • Example :

INITIALISATION
xx :: INT & / * xx is entire * /
yy :: BOOL / * yy is boolean * /

In order to calculate the checksum of this INITIALISATION clause, the following data is given to the MD5 algorithm sequencially:
« xx
« ::
« INT
« &
« yy
« ::
« BOOL

Supplement on lexical analysis on record expressions

A problem arrises for the lexical analysis of record elements because the nature of the ‘:’ character chosen to delineate labels of associated expressions already has a semantic in B (lexème L_BELONGS handled by the analyzer LR, binary operate, associative to left, priority 30) different than the one wanted for records (lexeme treaty by the high level parser).
To resolve this, we introduce the L_LABEL_COL lexeme, that represents the ‘:’ character in record expressions, and that has the wanted semantic.
The lexical analyzer converts, during an auxiliary pass, all L_BELONGS present at the first level of records expression (rec(. . . ) or struct(. . . )) into L_LABEL_SCOL.

Release of in-memory’s files

The « load_sct » table is released, as well as the position FIFO.

Second part : High-level syntaxic analyser

Chapter 6 : Static structure

Externs interfaces

Syntaxic analysis of a source file

  • Prototype
   T_betree *function compiler_syntax_analysis(
   const char *input_file,
   const char *second_input_file = NULL) ;

Description

The « compiler_syntax_analysis » function reads a source file, makes the syntax analysis and returns a BeTree. Parameters allow to indicate the file that is to be analyze, like described in paragraph 4.1.1.
It calls the lexical analyzer, described in part I, then the component syntax analysis function, described in paragraph 6.2.
If the source file is a « multi-component » file, the syntax analysis of all components present in the file is released. As many syntax BeTrees are created as the number of components in the file. The function returns the BeTree corresponding to the first component of the source file, the other BeTrees being accessible with BeTree manager.

Syntaxic analysis of a component

Prototype

   T_betree *function syntax_analysis(
   T_lexem *first_lexem,
   const char *new_file_name)

Description

This functions’ input is a lexeme flow and the file name that this flows represents< It makes the global syntax analysis of this file, and produces the associated BeTree. At the end of the analysis, the function returns the BeTree, or NULL in case of an error.

Algorithm

This function creates an instance of « T_betree », and analyzes the first lexeme of the file. If it’s a « L_MACHINE », a « L_REFINEMENT » or a « L_SPECIFICATION », the « T_machine » constructor is called. If not, an appropriate error message is produced.

 

Chapter 7 : Dynamic structure

Basic functionment of analysis

Responsabilitiss functioning

Each class representing an entity, analyzed by the high-level syntax analyzer, is </u>responsible</u> for its syntax analyzer.
In other words, a constructor must make the syntax analysis of the whole portion of source code that corresponds to it.
For example, the « T_op » class constructor is responsible of the syntax analysis of the considered operation, since the declaration of any output parameters of the operation, and until the END that signifies the end of the operation.

Progress in the lexeme flow

By convention, class constructors receives the address of the current lexeme in the lexeme flow as a parameter . This lexeme must be the first lexeme of the entity to be analyzed.
The constructor must then make the syntax analysis corresponding to the complete entity, and then store in the current lexeme pointer the lexeme immediately following the last lexeme of the entity. Picture 7.1 give an example of the progression in the lexeme flow.

Recursive procedural analysis technique

Principle

A multitude of small syntax analyzers

The principle basic applications exposed in section 7.1 leads to the writing of small dedicated syntax analyzers in each class.

The majority of classes possess a « syntax_analysis » method, in charge of executing the syntax analysis corresponding to the instances of this class. Thus, paragraph 7.2.2 gives the algorithm used in the « T_op » class « syntax_analysis » method.
The advantage of this technique is that syntax analyzers are small and can easily be debuged, because we know on each steps which lexemes can be input. The corollary is that we can produce detailed error messages and even say which input we would have liked to have.
Thus, we can not only implement a mechanism for error detection, but also implement techniques for automatic correction.

  • Specialized functions

Furthermore, a certain number of specialized functions allows the request of syntax analysis for an object of which we know only generic type (substitution, predicates, . . . ). Those functions are described in paragraph 7.3.

  • Chaining principle

Class constructors all take the address of the first & last elements of the list in which they must belong as parameters. Thus, by using automatic insertion services of the « T_item » class, objects created are automatically stringed at the right place.
For example, when running syntax analysis of « T_if » classes, ELSE branches are obtained by calling the constructor of the « T_else » class, in which the address fields « first_else » and « last_else » of the « T_if » instance become parameters during the analysis.

Example : syntaxic analysis of an operation

The BNF recognize by this function is the following :

  [ decla_in_params] nom_op [ '(' decla_out_params ')' ] = substitution

The following algorithm is used :
– Move to the next notch to find out if we have an output parameter or already have the name of the operation, i.e. decla_in_params :
~ If we have a « L_COMMA » or a « L_RETURNS », it’s an output parameter
~ If we have a « L_EQUALS » or a « L_OPEN_PAREN », it’s an operation name
~ If we have anything else, it’s a syntax error.

– Depending on the nature of this lexeme :
~ If it’s a « L_COMMA » or a « L_RETURNS » : the operation has output parameters. We analyze them with the following loop :
~ If the current lexeme is not an identifier, produce an error message that says we were waiting for an output parameter.
~ If not, call « syntax_get_ident » who creates the associated identifier.
~ We study the current lexeme :
If it’s « L_COMMA » , loop continues, i.e. still waiting for additional output parameters.
If not, leave loop.
~ Repeat the loop

– The current lexeme must be a « L_RETURNS ». If it’s not, produce an error message. If it is, advance another notch in the lexeme flow. The current lexeme is the name of the operation : it’s called « syntax_get_ident ».
~ If it’s a « L_EQUAL » or a « L_PAREN », everythings all right, it’s an operation without output parameters. Continue to the next step.
~ If not, produce an error message that indicates the header of the erroneous operation.

– Then, we analyze the operation name, which must be a L_IDENT
– If the current lexeme is a « L_OPEN_PAREN », the operation has input parameters. We analyze similar way than the output parameters.
– The current lexeme must now be a « L_EQUAL ». If it’s not we produce the adequate error message.
– We move up a notch in the lexeme flow and we call the « syntax_get_substitution » function to recover the body of the operation. We set in its parameters the adresses of fields « first_body » and « last_body » in order to automatically string the obtained substitutions in the object.

 

Specialized syntaxic analysis functions

= Expression analysis

  T_expr *function syntax_get_expr(
  T_item **adr_first,
  T_item **adr_last,
  T_item *father,
  T_betree *betree,
  T_lexem **adr_cur_lexem) ;

Instanciation analysis

  T_expr *function syntax_get_instanciation(
  T_item **adr_first,
  T_item **adr_last,
  T_item *father,
  T_betree *betree,
  T_lexem **adr_cur_lexem) ;

Simple term analysis

  T_expr *function syntax_get_simple_term(
  T_item **adr_first,
  T_item **adr_last,
  T_item *father,
  T_betree *betree,
  T_lexem **adr_cur_lexem) ;

Identifier analysis

  T_ident *function syntax_get_ident(
  T_ident_type new_ident_type,
  T_item **adr_first,
  T_item **adr_last,
  T_item *father,
  T_betree *betree,
  T_lexem **adr_cur_lexem) ;

Note that it’s the appellant that determines the identifiers nature. Indeed, the nature of the clause in current analysis determines the identifiers nature. Thus, when running CONCRETE_VARIABLES clause analysis, identifiers created are of ITYPE_CONCRETE_VARIABLE type, . . .

Operations analysis

  void function syntax_get_operations(
  T_item **adr_first,
  T_item **adr_last,
  T_item *father,
  T_betree *betree,
  T_lexem **adr_cur_lexem) ;

Predicate analysis

  T_predicate *function syntax_get_predicate(
  T_item **adr_first,
  T_item **adr_last,
  T_item *father,
  T_betree *betree,
  T_lexem **adr_cur_lexem) ;

Analysis of a parameter type of machine, or a predicate

  T_predicate *function syntax_get_machine_param_type_or_predicate(
  T_item **adr_first,
  T_item **adr_last,
  T_item *father,
  T_betree *betree,
  T_lexem **adr_cur_lexem) ;

Analysis of a constant type, or a predicate

  T_predicate *function syntax_get_constant_type_or_predicate(
  T_item **adr_first,
  T_item **adr_last,
  T_item *father,
  T_betree *betree,
  T_lexem **adr_cur_lexem) ;

Analysis of a variable type, or a predicate

  T_predicate *function syntax_get_variable_type_or_predicate(
  T_item **adr_first,
  T_item **adr_last,
  T_item *father,
  T_betree *betree,
  T_lexem **adr_cur_lexem) ;

Substitution analysis

  T_substitution *function syntax_get_substitution(
  T_item **adr_first,
  T_item **adr_last,
  T_item *father,
  T_betree *betree,
  T_lexem **adr_cur_lexem) ;

Third part : Syntaxic analyser LR

Chapter 8 : Static structure

Internal interface

Syntaxic analysis of a source file

Prototype

  T_item *function syntax_call_LR_parser(
  T_item **adr_first,
  T_item **adr_last,
  T_item *father,
  T_betree *betree,
  T_lexem **adr_cur_lexem) ;

Description

The « syntax_call_LR_parser » function calls the LR analyzer in order to analyze the formula from

  • adr_cur_lexem.

The LR analyzer returns the associated formula and updates *adr_cur_lexem on the first lexeme that follows the formula, or returns NULL in case of an error.

Modeling of automaton states

  typedef enum
  {
  LR_STATE_E0 = 0,    // State E0
  LR_STATE_E1,          // State E1
  LR_STATE_E2,          // State E2
  LR_STATE_E3,          // State E3
  LR_STATE_E4,          // State E4
  LR_STATE_E5,          // State E5
  LR_STATE_E6,          // State E6
  LR_STATE_E7,          // State E7
  LR_STATE_E8,          // State E8
  LR_STATE_E9,          // State E9
  LR_STATE_E10         // State E10
  } T_lr_state ;

Modeling of automaton stack

An LR automaton use 2 stacks when running a file analysis : a state stack, and a symbol stack. The LR analyzer uses, in addition, a memorization stack of opening and closing symbols, in order to detect problems of unclosed brackets.
The B Compiler defines the generic « T_lr_stack » class (template) , that models a generic LIFO element stack of a T class passed in parameter.
This class exports the followings methods :
– Stack creation : T_lr_stack()
– Stack destruction : ~T_lr_stack()
– Stacking an element : void function push(T new_item)
– Un-stacking an element : T function pop(void)
– Un-stacking n element : T function pop(size_t nb_items)
– Stack reset : void function reset_stack(void)
– Get an element at the determined depth of the stack without un-stacking (by convention, depth = 0 represents the top of the stack) : T function get_depth(size_t depth)
– Get the top element without un-stacking : T function get_top(void)
– Is the stack empty ? : int function is_empty(void)
Templates are used according to the explicit instantiation semantics, as explained in the GCC documentation. This explains the following line of s_lr.cpp :

   #define DEFINE_TEMPLATES
   #include "s_lrstck.cpp"

The « s_lrstck.cpp » module that defines templates is not quite like others because you use « #include » of this source file for templates instantiations. It’s never compiled like an autonomous module. It therefor does not have a usual structure because it’s included by others sources files. The #ifdef DEFINE_TEMPLATES at the beginning of the file avoids an untimely autonatic compilation by Visual-C++. Corollary : you must write #define DEFINE_TEMPLATES, then #include « s_lrstck.cpp » when instantiating explicit templates You are therefor obliged to explicitly instantiate the three types of stacks used :

   template class T_lr_stack<T_lr_state> ;
   template class T_lr_stack<T_object *> ;
   template class T_lr_stack<T_lexem *> ;

The advantage of this approach is to use a portable template mechanism and that you fully control.

Function of analysis LR

Prototype

   T_item *function LR_analysis(
   T_item **adr_first,
   T_item **adr_last,
   T_betree *betree,
   T_lexem **adr_cur_lexem)

Algorithm

– Allocation :
~ of a states stack « state_stack ».
~ of a symbols stack « symbol_stack ».
~ and of an opening stack « open_stack ».

– State stack initialization : state_stack->push(LR_STATE_E0)
– LR Analysis main loop:
~ Obtaining current state.
If opening stack is not empty:
If the current lexeme is a « L_SCOL », it must be transformed into a « L_LR_SCOL ».
If current lexeme is a « L_PARALLEL », it must be transformed into a « L_LR_PARALLEL ».

~ Call of the treatment associated with the current couple ( state, symbol ), that updates the variable « goto_next_lexem », that determines progression of the LR analyzer in the lexeme flow for the next step.
~ If treatment say analysis is finished :
Correction of produced tree, as specified at paragraph 10.2 of [CPL6].
Stringin of the result.
End of analysis.

– We run to the next lexeme, previous lexeme or we stay on the same lexeme, depending to the value of « goto_next_lexem ».

Fourth part : Semantic analyser

Chapter 9  : Static structure

Prototype

   T_betree *function compiler_semantic_analysis(T_betree *syntaxic_betree) ;

Description

The « compiler_semantic_analysis » function make semantic analysis of a syntactic BeTree. The enriched BeTree is returned if successfull. In case of an error, the function returns NULL.

Steps of semantic analysis

Picture 9.1 shows different phases of semantic analysis of a component.

Chapter 10 : Compliance analysis

Loading of required machines

Image 10.2 illustrates the loading of required machines

Prototype

   T_betree *function load_required_machines(T_betree *betree)

Principle

The « load_required_machines » function loads required machined with references update (via T_used_machine) in the BeTree. Machines are loaded with the « compiler_syntax_analysis » function. This function use the « tmp2 » field of « T_betree » instances, as a marker so as to not be executed 2 times on the same component : – If tmp2 == TRUE the function as already been called, nothing is done
– If tmp2 == FALSE the function was never called : Do the treatment, and put « tmp2 » to TRUE

Remember that field is set to FALSE in the constructor of class « T_object ».

Algorithm

Abstraction
We load the abstraction, if there is one, then : – Update the « ref_abstraction » and « ref_refinement » fields of the concerned machines.
– Recursively call « load_required_machines » for abstraction.
– Update the « ref_specification » field of the machine in current analysis by backing up through « ref_abstraction » fields.
– Verify that the abstraction is a specification or a refinement.

Others required machines
For all referenced machines in SEES, INCLUDES, IMPORTS, EXTENDS and USES clauses :
– Ask BeTree manager if the corresponding BeTree is loaded.
– If not, Load the BeTree. BeTree manager takes it automatically into account.

Link between BeTrees
During the loading of Betree, the seen_by, included_by, imported_by, extended_by, used_by lists of each BeTrees are updated, as illustrated in picture 10.3.

Compliance analysis on component

Prototype

   T_betree *function component_seman_analysis(T_betree *betree)

Principle

The « component_seman_analysis » function makes the semantic « component » level analysis of a syntactic BeTree. The enriched BeTree is returned if the analysis is successful. In case of an error, the function returns NULL.

Algorithm

The B compiler currently doesn’t verify compliance in this stage, all checks are realized at the end of the semantic analysis.
In the long run, some checks that are not carried out for the redundage of the transcoding string will have to be realized in this function.

Project control

Prototype

static void function global_project_analysis(void)

Principle

This function verifies that a machine instance is not imported several times in the project.

Algorithm

– Run through the BeTree list, obtained from the BeTree manager .
– For each element from the list, we ask component list that import this BeTree with the « get_imported_by » method.
– Check the number of elements on this list : if there is more than one, Send an error message.

Chapter 11 : Anti-colision control

Inherit on environment of includes machines

Prototype

   void function T_machine::import_included_environment(T_machine *included_machine)

Principle

The « import_included_environment » function retrieves the environment of an included machine. It’s called for each loaded BeTree, by means of a loop.
This loop runs through the BeTree list in reverse, in order to respect dependencies order, because if A uses B, then loading the A BeTree caused the loading of the B BeTree (see pictures 10.2 and 10.3 for loading examples).

Algorithm

In this algorithm, we suppose that a component A includes a component B. The following entities are inserted in A from B’s data :

  • Recovery of concrete constants

All of B’s concrete constants are recovered in the following manner :
– In accordance with the EREN 2 requirements, constants are not renamed, a « T_ident » is created by calling cloning constructor of this class.
– B constants are included only once, even if there are many instances of B.

Recovery of Abstract constants The same algorithm as the one for the recovery of concrete constants is used.

  • Recovery of Concrete variables constants

All abstract variables are recovered in the following manner :
– If B is included with renaming, a « T_renamed_ident » is created.
– If not, a « T_ident » is created by calling the cloning contructor of this class.

Recovery of Abstract variables The same algorithm as the one for concrete variables recuperation is used.

Recovery of abstract and enumerated sets Much like other constants, sets are not renamed, the same algorithm as the one for the recuperation of concrete variables is used.

Collages detection

Prototype

   void function T_machine::lookup_glued_data(void)

Principle

Function «  »lookup_glued_data » runs through the data list of the machine, and detects those that are glued by homonymy.

Algorithm

  • General algorithm

– Look, among the abstract constants of abstraction, for homonyms of an imported, included or extended machinery constant.
– In order to do so, the auxiliary « internal_lookup_glued_data » function is called, the component abstraction concrete constant list, and the component abstract & concrete constant lists being considered as parameters. This function is described in the next paragraph.
The functions goal is to detect possible collages, and update the adequate list if failed.
– The same work is done for concrete constants, abstract variables, concrete variables and sets.
– For the covered machines, we only look for sets and abstract or concrete constants.

  • Auxiliary constants

The « internal_lookup_glued_data » function has the following prototype :

   void function T_machine::internal_lookup_glued_data(
   T_ident *list_ident,
   T_item **adr_first_conc,
   T_item **adr_last_conc,
   T_item **adr_first_abs,
   T_item **adr_last_abs)

It runs through the « liste_ident » list, and verifies for each elements if they are present in a required component.
If it is, identifier is glued. It is inserted in the « concrete » identifiers list (adr_first_conc, adr_last_conc) or in the « abstract » identifiers list (adr_first_abs, adr_last_abs), depending the nature of the required component. The « def » and « ref_glued » fields of the « glued » identifier is updated with its « definition », meaning with a reference on the identifier of the required machine.
Before each collage, a verification is made to see if both identifiers can semantically be glued. For example, we can’t glue two sets that don’t have the same elements.
These verifications are done by the following function : check_glued_compatibility (

   T_ident* original_ident,
   T_ident* glued_ident)

Inherit of abstraction environment

Prototype

   void function T_machine::import_abstract_environment(void)

Principle

The « import_abstract_environment » function recovers the abstraction environment of the component, if there is one.

Algorithm

– Recovery of abstraction concrete constants
~ For this, we run through the abstraction concrete constants list (« ref_abstraction->get_concrete_constants() » method).
~ All non-presents constants in the machine are added thanks to the « T_item » cloning constructor. Those which are not present are not inherited, because they are, normally, glued.

– Recovery in the same way of abstraction concrete variables and sets.
– Then, Run through the list of abstract constants of the component. If the abstraction defines the same constant, there is implicit collage. In this case, an update of the fields « ref_glued » and « def » is done, as in paragraph 11.2.3
– In the same way, we detect collages for abstract variables.

Anti-collision controls

Prototype

   T_betree *function collision_analysis(T_betree *betree)

Principle

The « collision_analysis » function makes an anti-collision analysis on a component. Here, we use collision verification algorithm of the [REF] document, the « hidden conflicts » of the first string are not taken into account.

Algorithm

The list associated to the component is created, as specified in [REF], a verification is made during the process to insure that there is no duplicate. For this, we use auxiliary « add_L_MCH, add_L_SEES, add_L_INC, . . . » functions that create the specified lists.
We manage a list of already inseted machines. In order to verify instances are studied only once time, we use the clock mechanism.

Secondary function of list adding

  • Prototype
   static void function add_list_link(T_ident *new_item,
   T_list_link **adr_first,
   T_list_link **adr_last)
  • Principle

This auxiliary function adds the identifier « new_ident » in the list which became a parameter, with non-collision control.

  • Algorithm

Tha adding takes placewss by means of the « T_list_link » mechanism.
In case of duplicate detection in the list, we must verify if the two identifiers i1 and i2 are in potential collision are pasted or not.
In order to do so, a verification is made to see if the « ref_glued » field of i1 is the same as the one for i2, and if the one for i2 is the same as the one for i1.
If one of those two tests is true, the identifiers are glued : there is no conflicts. If not, we produce an error message to warn of the conflict between i1 and i2.

Chapter 12 : identifier resolution

Prototype

   void function T_ident::solve_ident(void)

Principle

The « solve_ident » method is a high-level method that looks for the definition of a non-resolved identifier.
The B compiler runs trhough the non-resolved identifier list by using the « get_ unsolved_ident » method of objects manager, and calls the « solve_ident » method for each element of this list.

Algorithm

Identifier searching

The algorithm consists in calling the virtual « find_ident » method described in paragraph 12.3.2 for the indentifiers father to resolve.
This virtual « T_item » class method verifies if the considered instance defines the indentifier that became a parameter.
If it returns NULL, then the father does not define the indentifier. The search then continues recursively by calling the method for the fathers father,… either until the indentifier definition is found, or until an element whos father is NULL is reached.
In this case, the Betree has been run through without succes, the indentifer is undefined, and the appropriate error message is produced.
In order to avoid asking an object if it define the identifier more than once, a clock mechanism is usedm stocked in the t;p2 field of the covered objects. For example, if we ask a « T_op », il will propagate the search to all the « T_ident » that modelise the parameters. In turn, each of these « T_ident » will ask its father, meaning th « T_op », if it defines the researched indentifier.

There is therefor a potentiel looping if the clock mechanism described in chapter 20 is not used.

Identifier searching method

  • Prototype
   virtual T_ident *function find_ident(T_symbol *name) ;
  • Principal

The virtual « find_indent » method specified in « T_item » provokes the recursive research of an indentifier in the considered object, according to the principals of responsibility and usual recusivity.
Warning, on the client level, the « find_ident » call must always be preceded by a « next_timestamp » call (i.e. change clocks) in order to reinitialize the non-looping mechanism.

Visibility control

Once an indentifiers definition D has been found, a verification must be made to see if this use does not violate the rules of visibilityu of the B language.
In order to do so, the following must be determined:
– The type, ¢, of the accessed entity (a formal parameter, a constant,…). To accomplish this, a search is made for the indetifiers definition in so as to know its nature, then we apply the conversio table on figure 12.1.
-The emplacement, ¤, of this entity’s definition (a seen machine,…). To realize this, « get_sees », « get_includes »,… methods are used to find the relation between the machine being analyzed and the machine defining I
-The context ª from where the access was granted (CONSTRAINTS clause, an operation,…). In order to do so, the « get_father » fields of I are ran through in reverse until one of the visibility table entity is found: an operation, an ASSERT, a clause,…

Then, the get_auth_with_details( ¢, ¤, ª) function is used to see the acess authorization A corresponding to the three previous parameters.
Finally, the « check_rights » function is used to verify that A is sufficient to acces D
If the rights are sufficient, I is resolved, its definition field is pointed on D. If not, a error message is produced explaining the violation of the visibility tables. The implementation of visibility tables et their elements is specified in paragraph 6.3 of the [CPL8] document.

Chapter 13 : BeTree correction

Prototype

   void function T_op_result::check_is_an_op_result(void)

Principal

Introduction

The syntaxic analyser does not know if an expression of f(x) type corresponds to a f function call with the paramater x (for example succ(1)), or if it corresponds to the access to the x index of a f table.
Thes two types of entities are modeled differently in the Betree: a function call is modeled by means of the T_op_result class, whereas a table is represented by means of the T_array_item class.
By default, the syntaxic LR analyzer only builds « T_op_result » instances, and leaves it to the semantic analyzer to change the « T_op_result » in « T_array_item » if needed.
That’s the task accomplished during the tree correction phase.

Method

The semantic analyser runs through the list of all the « T_op_result » that were created, by means of the « get_op_result » method of the object manager.
For each element of this list, the « check_is_an_op_result » method is called. This function executes the following checks: A T_op_result can only be valid if ref_builtin != NULL. If not, the element is in fact an access and, therefor a T_array_item. In this case, a verification must be made to insure that op_name does not point towards an operation name (ITYPE_OP_NAME) because the syntax x:= f(y) where f is an operation is illicit.

Algorithm

Principal
-If ref_builtin is positionned, then it’s a call to a predefined function, and the knot is correct.
-If not, a T_array_item i0 need to be created, by calling the constructor of this classe that uses as a parameter the T_op_result i that needs to be corrected.
Then all the references on i need to be changed into references on i0. In order to do so, the two following treatments need to be executed:
~If a list has become a parameter, then i is exchanged for i0 in the list by means of the exchange_in_list method.
~Run though all of i‘s fathers fields using metaclasses. All the fields that reference i are modified to reference i0.

-Finalement, the ref_array_item of i is pointed on i0

Chapter 14 : Data typing

Extern interface

Prototype

   T_betree *function type_check(T_betree *betree)

Principle

This function verifies the types of the Betree of its parameter

Algorithm

The Verification of type does a double check:
– Type inference on the concerned Betree’s root.
– Verification of the STRING type: this type is only allowed to portray onperation input parameters as types
The type inference is realised by means of the virtual type_check function of the T_item class.
The responsability principal is used once again. The type_check method of each class is responsible for it’s own type verification, propagating, if needed, this verification to the contained elements.
In this chapter, the different type_check methods will be studied.

Type check for T machines

-The instances of this class posess a type_checkes field, initialized at FALSE in the constructor, that allows us to know if the method has already been called by this instance (this is possible because a projet machine can be referenced many times by different modules:
~At the beginning of the analysis, the value of this field is tested. If TRUE, the analyze has already been done, and the treatment stops.
~If not, le field value is set to TRUE and the analysis begins.

-To begin, the type_check of the required machines is called (SEES, INCLUDES, IMPORTS, EXTENDS, USES, and abstraction).
-Then checks are done on the component itself:
~The Setof(atype(ENS)) type is allocated to the ENS formal set parameters ~The same is done for the SETS that aren’t enumerated sets, and in addition the limits are positionned by means of the T_bound class.
~Succesive type_check are then executed on:
The CONSTRAINTS clause
The VALUES clause set
The PROPERTIES clause
The PROMOTES clause
The VALUES clause constants
The INVARIANT clause
The ASSERTIONS clause
The INITIALISATION clause substitutions
Operations

In the end, the following checks are executed:
– Verification that all variables and constants are typed
– Verification of the variable & constant type glued in the abstraction and the required machine compatibility.

Le following check are not realised in the actuel version of the B Compiler:
– Verification of the existence of a valuation for unglued constants and abstract sets.
– Verification of the existence of an initialization for unglued variables.

Type check for substitutions

Principle

The type_check methods for substitutions implement the VTYPE3 checks of the [CPL8] specification.

Example : type check for T class let (VTYPE 3-14)

– Verify that the identifiers introduced in the LET are distinct.
– The type_check methods are called for each of these identifiers.
– All the valuations are ran through:
~A verification is made to see if the identifier in the left part are only identifiers introduced by LET.
~A verification is made to insure that each identifier is only valued once.
~A verification is made in order to see if the identifiers used to type or value are already typed (T_ident::check_type() function) ~The type)check method is called for each valuation.

-The type_check_substitution_list is called on the LET body. This function is described in the following paragraph.

Substitutions list type_check secondary function

– Prototype :

   void function type_check_substitution_list(T_substitution *list)

– Principle : This function does the type_check of the substitution list used as a paramater.

– Algorithme : The type_check method of each element from the list needs to be called. Furthermore, if two substitutions S1 and S2 are called at the same time, a verification must be made to insure that the variables allocated by S1 are distinct from the variables allocated by S2, and another verification must be made in order to verify that the operations used by S1 do not stem fron the same included machine instance as S2.
In the general S1||S2||S3||Sn case the verification procedes by verifying this it is not the case with S1 and S2, then with S1 and S3,… then with S1 and Sn.
The verifications for S2 with S3 will take place during the next iteration.
The unitary verification is undergone by means of the parrallel_checks function.
-The parallel_checks function verifies that in two parralel substitution S1 and S2, the modified variables are different:
~In order to do so a modified variable list is created by the two substitutions and a verification is made to insure that the lists are disjointed.
~In order to accomplish this, two different clocks are used for the t1 and t2 substitutions ~If an identifier is modified by S1, its tmp2 field is set to t1. If it is modified by S2, as check is made to see if its tmp2 field has a value of t1. If that is the case, there is a conflict. If not the t2 value is allocated to tmp2.

-The parallel_checks function also verifies that in two parallel substitutions S1 and S2S1‘s operations don’t come from a same machine instance than the S2operations. The verification in 2 steps:
~Creation of a T_list_link with the machine instances from which the S1 operations stem.
~Verification that the machine instances from which the S2 operations stem from are not in the T_list_link.

Type check for predicates

Principle

The type_check methods for predicates implement the following [CPL8] specification checks:
– The typage predicates implement ITYPE checks.
– The other predicates implement VTYPE1 checks
The VTYPE1 checks consist in recusively propagating the checks inside the predicates because only typage predicates allow identifier typing.
ITYPE check are studied in the next paragraph.

Type check for typage predicates

This task is realised by means of the T_typing_predicate class type_check method, that implement ITYPE checks.
This method calculates identifier types in the left part, types in the right part, and allocates types by means of the T_expr set_type method described in paragraph 14.5.2.
The type_check_loop function does this work. It verifies that there are as many type on the left part as on the right part of the predicat, and starts up unitary typage: single_type function.
This function verifies that the identifiers on the right part are typed before being used, so as to accomplish this, it uses the virtual check_type function.

type check for expressions

Principle

For the expressions, the type verification is limited to the type calculation. This role is appointed to the virtual T_expr make_type method, that calculates the type of each expression as specified in the [CPL8] VTYPE 2 verifications, and that verifies that all identifiers used in the expression are typed.

Type storage

The expression types are stocked in their B_type fileds inherited from the T_item class
In the particular case of identifier, the type is stocked in the definition, as described in [CPL8] chapter 15 and illustrated in figure 14.1. The allocation of type is then preceded by a compatibility verification with the possible preceding type.
The T_type class defines the virtual is_compatible_with method that allows us to know if two types are compatible. This method is used in the T_ident instances set_B_type method.

Example: make type for the classe T op result

Prototype : void function T_op_result::internal_make_type(void)
The virtual T_op_result::internal_make_type, called by T_expr::make type has a double role:
– Verify the number and the type of the parameters
– Build the operator type
These operations being specific to each operator, we call the T_op_result::vtype_xxx appropriated to the value of the lex_type field. For example, if lex_type == T_sons, then the T_op_result::vtype_sons(keyword) is called.

Verification of the number and type of the parameters
This task is done by the appropriate method whose name is in the form:

  T_op_result::vtype_xxx, where xxx is the name of an operator.

The number of parameters is given by the nb_in_params field, it is neccesary that its value corresponds to to the specification value.
When a parameter type is a complex construction, the verification is appointed to a virtual T_type (or derivative) class that rewiews each type while verifying each element of the construction.
For example int T_type::is_a_tree_type(void) returns TRUE if the type is in the form:

  ª(ª(INTEGER¤INTEGER)¤T)

Construction of the operator type This task is done after the parameter verification, in the vtype_xxx function. The type is built by creating new instances of a class derived from the T_type. In order to do so, either the constructors, or the T_type::clone_type cloning method (see section 14.6) is used.
When the construction is complex, the work is given to functions. For example:

  - T_setof_type* function create_a_sequence_type crée le type: ª(INTEGER¤T) 

  - T_product_type* function create_a_tree_type crée le type: ª(ª(INTEGER¤INTEGER)¤T)

Modeling type

The types stocked in the expressions are specific to each expression. As such, all type calculation functions stocked in expressions build a result that is a private copy of the type that is returned, as illustrated in figure 14.2.
Thus, each expression is the « owner » of its type and can therefor insert it in a list, modify it in case of valuation,… at will.
To obtain a private copy of a type, the « custom » T_type::clone_type() cloning method and not the generic cloning algorithm for historical reason (this method was developped before generic methods) and because it is more efficient in this pparticular case.

Verifications on STRING types

The STRING type is allowed only for typing operation input parameters.
The verification algorithm is as follows:
-All STING type expressions are systematically prohibited, except for these two expression types:
~ T_ident
~ T_litteral_string

– For the indentifiers, the verification is made during the typage. The only form of typage allowed is: ident : STRING, if the ident is an operation input parameter.
– The STRING type to instantiate the formal parameters of the required machines is prohibited.

prohibition of expressions of type STRING

The virtual void T_expr::prohibit_stings_use() function is called at the end of the T_expr::make_type function, that is an obligatory passage point after expression typage.
In the general case, the T_expr::prohibit_strings_use() function, produces an error message if the expression type is STRING or a constructor that uses this type.
It is redefined for T_ident and T_litteral_string functions. In thes cases, it does nothing.

Verification during identifier typage

After having typed the identifier, the c_ident::check_string_uses(int is_typing_with_belong) function.
This function provokes an erreur message in the following cases:
– The identifier is of the STRING type and its definition is not an operation input parameter.
– The identifier is of the STRING type and the is_typing_with_belong is set to FALSE. Meaning that the identifier has not been typed with the « belong » predicate.
The verification is done in the places where identifiers can be typed, that is to say in the following typage substitution functions:
– L’identificateur est du type STRING et sa définition n’est pas un paramètre d’entrée d’opé- ration. – L’identificateur est du type STRING et le paramètre is_typing_with_belong est positionné à FALSE. C’est à dire que l’identificateur n’a pas été typé avec le prédicat appartient ».

La vérification est faite aux endroits où les identificateurs peuvent êtres typés, c’est à dire dans les fonctions des substitutions de typage suivantes :
– T_affect::type_check
– T_becomes_member_of::type_check
– T_becomes_such_that::type_check
Or in the following typage predicate function:
– T_typing_predicate::type_check

Instantiation verification of parameters

In the T_used_machine::type_check function, a verification is made to insure the instantiation parameters are not of the STRING type.

Fifth part : B0 verification

Chapter 15 : Syntaxic controls

The application of the basic principles enunciated in section 7.1 leads to the writing of small dedicated syntaxic analysers.

Controls on predicates

In an implantation, the predicates concerned by a B0 check are:
– The substitution condition IF (and ELSIF)
– The substitution condition WHILE
– The condition of a bolean expression bool(condition)

These check will therfor be managed by higher level checks concerning instances of:
– T_if
– T_else (modeling an ELSIF)
– T_while
– T_op_result (modelising a predifinedd bool operation call)

Concerning the first three points, in the case of an instance descending from an implantation (T_machine instance with a MTTYPE_IMPLEMENTATION machine type attribute), the corresponding class type_check method calls to the predicate that needs to be checked (the condition) the virtual recursive method:

  virtual int function T_item::syntax_check_is_a_B0_predicate(...);

This returns TRUE if the predicate is a B0 language predicate.
Concerning the fourth point, the above virtual recursive method is called during the bool(condition) expression’s analysis in order to respect the basic princinples stated in section 7.1
This allows a complete targeting of the checks and as a result manage the different exceptions (The invariant of a While substitution is not restricted to conditions for example)

Controls on expressions

In an implant, the expressions concerned by a B0 check are:
– The expressions representing the effective parameters in the T_used_machine instances
– The expressions representing the valuations in the T_valuation instances
– The expressions representing the selections in the CASE substitutions (in the T_case instances)
– The expressions on each side of the affectations in the devien_egal substitutions (in the T_affect instances)
– The expressions representing the affective input parameters of the appel_operation substitution (in the T_op_call instances)

Still in the concern of targeting the checks, these are therefor managed by high-level check concerning the following instances:
– T_case,
– T_affect,
– T_op_call,
– T_used_machine,
– T_valuation.

This means that in the case of a descending implantation, the type_check method of the corresponding classes check the verifications that are to be made (In the same way as the condition checks, this targeting of checks allows for a management of the different exceptions.)

Virtual methods used for controls

For the needs of the different recursive check that are to be made, a certain number of virtual recursive methods are necessary. Their role is to recognize the expression of same nature as the BNF. These methods possess a parameter of T_B0_context type that describes the contexte of the syntaxic reconnaissance : a simple term has additional restrictions on its nature, in the case of a maplet indication for example. They possess other parameter which will be mentionned in chapter 18.

These are:

Recognition of a B0 expression in general

  virtual int function syntax_check_is_a_B0_expression(...)

Recognition of a simple term

  virtual int function syntax_check_is_a_simple_term(...)

Recognition of a term

  virtual int function syntax_check_is_a_term(...)

Recognition of a boolean expression

  virtual int function syntax_check_is_a_bool_expression(...)

Recognition of a maplet expression

  virtual int function syntax_check_is_a_maplet(...)

Recognition of a board expression

  virtual int function syntax_check_is_an_array(...)

Recognition of a borad access

  virtual int function syntax_check_is_an_array_access(...)

Recognition of a range

  virtual int function syntax_check_is_a_range(...)

Recognition of a singleton (for a constant board expression)

  virtual int function syntax_check_is_a_singleton(...)

Recognition dof an arithmetic expression

  virtual int function syntax_check_is_an_arith_expression(...)

Recognition of an access to a record in extension

  virtual int function syntax_check_is_an_extension_record_access(...)

Recognition of an record expression in extension

  virtual int function syntax_check_is_an_extension_record(...)

Chapter 16 : Semantic checks of concrete data typage

Principles

For each family of concrete data, the principle of the checks is exposed. These checks are done on all the components: abstract machines, raffinements, and implatations. Indeed, the typage of concrete data, wherever it is located, is an integral part of the B0 language.
Thus, for a given machine (the Betree managers allows us to browse through them easily), the following virtual recursive methods (defined in the T item classes) are called:

Case of checks on concrete constants

   void function T_machine::concrete_constant_type_check(void);

We access the elements of the PROPERTIES clause, that is a conjunction of typage predicates (T typing predicate instances). A call is made on this predicate conjunction of the virtual recursive method:

   void function T_predicate::concrete_constant_type_check(void);

This method is redefined in the T_typing_predicate class in the following manner:
– If the typed indentifier (T ident instance) is not a concrete constant (the indent type field of the identifier is different than ITYPE CONCRETE CONSTANT, meaning the identifier is considered an abstract constant), the analysis is stopped.
-The identifier is accessed and its B type that is checked : the following virtual recursive function is called

   int function T_type::is_concrete_constant_type(void);

That returns TRUE if the type is a valide type for a concrete constant.
– The type of typage predicates is checked (∈, =, ⊂ are authorized), and, depending on which, the corresponding typage expression:
~ ∈: call of the following virtual recursive method

  int function T_expr::is_belong_concrete_data_expr(void);

That returns TRUE if the typage expression is valid ~ = : call of the following virtual recursive method

  int function T_expr::is_equal_concrete_constant_expr(void);

That returns TRUE if the typage expression is valid ~ ⊂: call of the following virtual recursive method

  int function T_expr::syntax_check_is_a_simple_set(void);

That returns TRUE if the typage expression is a simple set.

Case of checks on concrete variables

   void function T_machine::concrete_variable_type_check(void);

The principle is identical, for the INVARIANTS clause.
The elements of the INVARIANTS clause, that is a conjunction of typage predicates (T typing predicates instances), is accessed. The following virtual recursive method is called on this conjunction:

   void function T_predicate::concrete_variable_type_check(void);

This method is redefined in the T_typing_predicate class in the following manner:
– If the typed identifier (T ident instance) is not a concrete variable (the ident type field of the identifier is defferent than ITYPE CONCRETE VARIABLE, meaning the identifier is considered an abstract variable), the analysis is stopped. – The identifier is accessed, as well as its B type that is checked : the following virutal function is called

  int function T_type::is_concrete_variable_type(void);

That returns TRUE if the type is a valid type for a concrete constant.
– The typage predicate type is checked (∈, = are authorized), and depending on which, the corresponding typage expression:
~ ∈: the following virtual recursive method is called:

  int function T_expr::is_belong_concrete_data_expr(void);

That returns TRUE if the typage expression is valid.
~ =: The following virtual recursive method is called:

  int function T_expr::is_equal_concrete_variable_expr(void);

That returns TRUE if the typage expression is valid.

Case of checks on machines parameter scalar

   void function T_machine::scalar_parameter_type_check(void);

The principle is identical, for the CONSTRAINTS clause. The checks here are systematic (no tests are necessary on the nature of the identifier), because the encountered identifiers are inevitably scalar parameters of the machine.
The elements of the CONSTRAINTS clause, that is a typage predicate conjunction (T typing predicate instances) are accessed. The following virtual recursive method is called on this predicate conjunction :

  void function T_predicate::scalar_parameter_type_check(void);

This method is redefined in the T_typing_predicate class in the following manner: – The identifier is accessed, as well as its B type that is checked : the following virutal recursive function is called

  int function T_type::is_scalar_parameter_type(void);

That returns TRUE if the type is a valid type for a machine scalar parameter.
– The typage predicate type is checked (∈, = are authorized), and depending on which, the corresponding typage expression:
~ ∈: the following virtual recursive method is called:

  int function T_expr::is_belong_scalar_formal_param_expr(void);

That returns TRUE if the typage expression is valid.
~ =: The following virtual recursive method is called:

  int function T_expr::is_equal_scalar_formal_param_expr(void);

That returns TRUE if the typage expression is valid.

Case of checks on input operations parameters

The operation input parameters being typed in a « precondition » substitution (T precond instance). The

  void function T_predicate::entry_parameter_type_check(void);

function is then called, in the T_precond::type_check() function on the instance predicate of T precond, that is a conjunction of typage predicates (T typing predicate instances) and of predicates in the broad sense of the word (that are proprieties).
This method is redefined in the T_typing_predicate class in the following manner: – The identifier is accessed, as well as its B type that is checked : the following virutal recursive function is called

  int function T_type::is_entry_parameter_type(void);

That returns TRUE if the type is a valid type for an operation input parameter.
– The typage predicate type is checked (∈, = are authorized), and depending on which, the corresponding typage expression:
~ ∈: the following virtual recursive method is called:

  int function T_expr::is_belong_in_op_param_expr(void);

That returns TRUE if the typage expression is valid.
~ =: The following virtual recursive method is called:

  int function T_expr::is_equal_in_op_param_expr(void);

That returns TRUE if the typage expression is valid.

Case of checks on output operations parameters

The operation output parameters being typed during their first utilization in the operation body, the

  void function T_type::is_exit_parameter_type(void);

function is then called, in the T_op::type_check() function, on the type of the T_op intance output parameters. This function retruns TRUE if the type is a valid type for an operation output parameter.
Notice: In this case there is no typage predicate.

Case of checks on local variables

In the same way, concrete locale variables are typed during their first utilization in the instructions. The

  void function T_type::is_local_variable_type(void);

function is then called, in the T_var::type_check() function, and if the T var instance is in an implementation, on the type of the T var local variables. This function returns TRUE id the type is a valid type for a concrete local variable. Notice: In this case also there is no typage predicate.

Type control

Auxiliary virtual recursive methods are necessary for type reconnaissance :

Is it a char type (no in the general case)

  virtual int function is_a_string(void);

Is it a boolean type (no in the general case

  virtual int function is_a_boolean(void);

Is it a concret int type (no in the general case)

  virtual int function is_a_concrete_integer(void);

Is it an overall abstract element (no in the general case)

  virtual int function is_an_abstract_element(void);

Is it an element of a package abstract or listed (no in the general case)

  virtual int function is_an_abstract_or_enumerated_set_element(void);

Is it an abstract or all listed (no in the general case)

  virtual int function is_an_abstract_or_enumerated_set(void);

Is it an interval whole or abstract (no in the general case)

  virtual int function is_an_integer_or_abstract_interval(void);

Is it a board type (no in the general case)

  virtual int function is_an_array(void);

Is it a record type (no in the general case)

  virtual int function is_a_record(void);

Is it a type of element simple set

  virtual int function is_a_simple_set_element(void);

Predicate typage control

Auxiliary virtual recursive methods are necessary. Their role is to recognize the same nature expression of BNF expressions. This method is: virtual int function is_a_string(void);

Is it a set of total functions

  virtual int function syntax_check_is_a_total_function_set(void);

Is it the expression « BOOL »

  virtual int function check_is_BOOL(void);

Is it the expression « STRING »

  virtual int function check_is_STRING(void);

Is it a set of record (structur conform to B0)

  virtual int function syntax_check_is_a_record_set(void);

Is it a set in extension of simple terms for the typage by membership

  virtual int function syntax_check_is_a_simple_term_set(void);

Coercion of non-use of abstract data for type a given concrete data

This constaint is imposed by the translator. During the typage expression checks, abstract identifiers are rejected. In order to manage the case of concrete tyuped data during their first use (local variables et mostly operations ouput paramaters because their typed in the abstractions), the constraint is verified at the B0 type construction : An erreur is caused if an abstract identifier is data member of the type B0 (type used by the translator).

Chapter 17 : Semantic check regarding B0 tables

A verification needs to be made in the following cases:
– equalities or inequalities on two tables (T binary op or T typing predicate instance)
– allocation of table data ( T affect instance)
– concrete constant of table type valuation (T valuation instance)
– operation call with one (or more) input/output parameter(s) of table type (T op call instance)

In order to insure that the considered tables are compatible in the implantations.

Checks principle

During the type inference phase, table expressions are typed, and their type possess’s all the information necessary to the compatibility check of the B0 tables.

The virtual

  virtual int function T_type::is_array_compatible_with(T_type *ref_type);

function executes the compatibility check between the calling type instance and the type that became a parameter.
This function is called in the T_affect::type_check() and T_op_call::type_check() functions if we are dealing with B0 tables.
Concerning the check on table equalities and inequilities, it is executed during the conditions check.
Finally, concerning the valuation of table type concrete constants, the compatibility check is done in the T_valuation::valuation_check() function described in the following chapter, and used for valuation checks.

In the case of whole type for a table index set, the check consists in verifying the syntaxic equility of the border expressions. In order to do so, the following virtual recursive function is used:

  virtual int function T_item::is_array_compatible_with(T_item *ref_item);

Maplet set particular case: in addition, a verification must be made to see if the maplets cover the totality of the considered tables definition domain. This verification is made during the syntaxic checks, and in particular after the syntaxic reconnaissance of a maplet set that complies with the B0. Remember that a maplet that complies with the B0 only has litteral whole numbers, litteral booleans, or enumerated values in its index. Depending on the table type, the expected index n-uplets list is created. The different table expression maplets are then compared with the expected n-uplets. A verification is made to insure that a total function between the table index and the expected n-uplets exists : The figure 17.1 on page 84 explains this check for a simple case.
Case of records that have table type labels: The

  virtual int function T_type::is_array_compatible_with(T_type *ref_type);

function is also called during the presence of records. It is the redefinition of this function for T_record_type instances that executes the compatibility checks for tables in the presence of table type labels.

Chapter 18 : Semantic, initialisation, valuation, and instanciation control

These checks only concern implantations.

Principles

For a given implantation, the following checks are executed:

Controls on variables initialisations

T_list_ident being a class that manages the identifiers list, the virtual recursive

  void function T_subst::initialisation_check(T_list_ident **initialised_ident);

function verifies thet the current instruction doesn’t contain any non-initialized variables. It takes as a parameter the T_ident’s instance list already initialized at the moment of the call, and enriches this list depending on the different paths of the B0 code (case of if and case instruction branchs), and depending on the variable list to initialize (global, and constructed beforehand). In the case of an operation call instruction the function verifies that effective parameters are initialized.
In the case of an allocation instruction, the function verifies the right expression doesn’t contain any non-initialized variables .
Finally, in the case of a « while » instruction, the function will control its body, but considers newly initialized variables as non-initialized on « while » output. Indeed, going through the loop at least once is not assured.
In order to do so, we parse expressions with the functions described in chapter 15. This is why those function have a T_list_ident ** parameter. When an identifier is met, the function verifies, if this identifier is in the variable list to initialize, that is is truly initialized.
This is done, firstly, to make checks on the instructions of the INITIALISATION clause, and secondly, to make checks on instructions that compose the operations.
Concerning the first case, the variable list to initialize is the list of all variables of the component that are not homonyms to variable instances of the imported machinery. Once this list is constructed, the function « initialisation_check » is called on the instructions of the INITIALISATION clause
The second case corresponds to the body of a T_var instruction. The variable list to initialize is then the T_var instance variable list. Checks are made in the T_var::type_check() function.

Example :

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

Valuations control

In the same way, the

   virtual void function T_item::valuation_check(T_list_ident *valued_ident);

function verifies that the « right part » of the valuations doesn’t contain non-valued constants. It takes as parameter the instances list of T_ident already valued at the moment of the call, and enriches this list of encountered valuations, considering the list of constants to be valued (global, and previously constructed).
This also allows to verify that they were all valued, and only once.
Furthermore, it makes checks on the authorized expressions on the right part of the valuations.
The algorithm is the following :
– An instance (global) of T_list_ident composed of the constant list the needs to be evaluated (all component constants non-homonyms to a data of similar viewed machine nature or imported) is constructed.
– The list of valuation expressions of the VALUES clause is recovered, and the virtual recursive valuation_check(T_list_ident *valued_ident) method is called on it. The algorithm parses the expressions with the functions described in chapter 15. This is why, these functions have a T_list_ident ** parameter. When an identifier is met, the function verifies, if this identifier if on the constants list to be valued, that it really needs to be valued.

Instanciations controls

The virtual recursive

  void function T_machine::instanciation_check(void);

function executes checks on the authorized expressions for the instantiation of formal machine parameters. The algorithm is the following: The content of the IMPORTS and EXTENDS clauses is recovered, and the following virtual recursive method is then called en it

  void function T_item::instanciation_check(void);

This method executes recursive checks on the used expressions used for the instantiations (thanks to reconnaissance functions described in chapter 15).

Sixth part : Managers

Chapter 19 : The object manager

Introduction

The object manager is used by the B compiler to stock global information that is reletive to the management of objects during one of its uses. Object meaning only the T_object instances. The other class instances are not managed by the Object manager (in particular, it does not manage « itself »).
The object manager is unique, it is created during the B compilers’ initialization. It is modeled as a T_object_manager class instance.
It is primarely used internally in the compiler to optimise tree browsing operations.
The object manager is modeled by means of the T_object_manager class.

Implementation of object manager

The T_object_manager class manages the following lists:
– An exhaustive list of all allocated objects. The objects are referenced by T_object_tag class instances that have the same inderection role as the T_list_link instances.
– A list of all identifiers, that are strung together by means of their next/prev_ident fields
This list is used by certains tools like Xref.
– A list of all unsolved identifiers, that are strung together by means of their next/prev_unsolved_ident fields.
This list is used during the identifier resolution.
– List of all T op result
This list is used during the tree correction.
– List of unsolved comments
This list is used during comment resolution, i.e. when the comment are linked to the Betree knots
– List of the unvalued abstract types
This list is used to propagate the valuation of an abstract type to all those that have been cloned from its model.

Chapter 20 : Clocks manager

Introduction

Specifications

The clock manager offers two principle services:
– Getting the current time
– Changing the time
The « getting the current time » service always returns the same value between two calls to the « changing the time » service. This last service modifies the current time, guaranteeing that the new time is different from all the previous times that have been furnished by this service.

Interest

Clocks are used in algorithms to mark the different phases of a loop: If two elements have the same clock, they were created in the same phase.

Application on clock manager

The clock managers offers the two services previously stated for two independant clocks.
The availability of two independant clocks enables the realization of check in imbricated loops.

API of clock manager

First clock

Getting the current time

  extern size_t function get_timestamp(void) ;

Changing the time

  extern void function next_timestamp(void) ;

Second clock

Getting the current time

  extern size_t function get_timestamp2(void) ;

Changing the time

  extern void function next_timestamp2(void) ;

Implementation

Each clock is implemented by means of a static whole variable, that is incremented during the time change demand.
In order to avoid any confusion between a void time and a non initialized field, the starting time of the two clocks both have values that aren’t void, respectively 1997 and 12.

Chapter 21 : Project manager

Introduction

Atelier B offers many functionalities that enable regrouping B sources in B projects, these projects can themselves be linked to other library projects.
The project manager is used to stock information relative to a project and to the library projects associated to that project.
The project manager is unique, it is created during the initialization. It is model by the T_project manager class.
The project manager is mainly used by Atelier B’s session moniteur to:
– Add B source files to the current project
– Find the B component dependencies.
– « Cut » B source files into components.
– Realise the functionalities of the Atelier B differential

Added a source file into a project

  • Présentation

The B source files can contain many B componants (« .mod » files). The add_file method of the T_project class adds a new B source file and the components it contains to a projet.

  • Algorithm

The add_file method starts by checking that there is no file that has the same name in the project.
The the compiler_dep_analysis function is called in order to know the list of components present in the Betree.
If this function detects a syntax error, the file is still added to the project in order to allow the user to add components even if they’re incomplete or incorect. Th component type and name are then determined depending on the name and suffixe of the B source file. A specification is created by default for the « .mod » files (multi-component).
If there is no syntaxic error, the Betree list is ran through a first time in order to see if there are no components present in the project.
If there are no redefine components, the Betree list is ran through a second time in order to add the components.

Dependencies search

  • Presentation

The project manager offers functionalities used by the Session Monitor of the Atelier B to construct graphs of the dependencies of B components between them.
The check_dependencies method of the T_file component class looks for dependencies for all the components present in the B source file modeled by this class.

  • Algorithm

– The check_dependencies method calls the compiler_dep_analysis function to construct the list of Betrees corresponding to the components present in the file. This compiler pass execute a minimum of checks; its goal is to construct a Betree with only the dependency clauses.
– Nonetheless, if this pass detects errors, the dependency search is stoped.
– Then the method executes a pass on the obtained Betrees.
– For each Betree:
~ A search is made for the component in the list of the components in the file.
~ It is possible the component has been added dynamically (In a multi-component file). In this case, it is added to a list of the project manager (add_added_component) to warn the session monitor.
~ It is also possible that the component has had a change of type (for example: specifcation becomes raffinement). In this case, an indicator is positionned in the project manager (set_modified_flag) to warn the session monitor.
~ If the component was already present in the file with the same type, a verification needs to be made to see if the component has been modified. In order to do so, the components checksum is compared to the checksum calculated by the compiler. If thes checksums are different, the checksum is set to NULL to warn the session monitor.
~ For all the components, the machine associated to the Betree is stored, in order to allow the session monitor to find the dependencies in the visibility clauses (get_include, get_imports, …).
~ All the components that are found when the Betree list is being ran through are marked using the clock manager.

– The method then looks for un-marked components. These components have been dynamically removed by the file user (multi-component case). These components are stored in the project manager (ass_removed_component) in order to warn the session monitor.
– If components have been removed or added dynamically, an indicator is positioned in the project manager (set_save_flag) to inform the session monitor that the projects structure has been modified and that he must therefor save it on a disk.

Cutting of B source files

  • Presentation

The Atelier B tools, with the exception of the B compiler, don’t know how to work on files containing more than one B component. The session monitor of the Atelier B uses the expand method of the T_file_component class to generate in a given directory files that only contain one component from the B source files.
This method executes the cutting in two different ways: – The first cutting gives components that are identical to the components in the B source file. This cutting is used by the translators of the Atelier B that don’t know how to work with files that contain more than one component.
– The second one gives components where the definitions have been expansed, et les renommages ont été parnethésés. This cutting is used by the old tools of the Atelier B (Type Checker,…).

  • Algorithm

– The expand method calls the compiler_dep_analysis function to execute the syntaxic analysis of the B source file.
– If this function detects an error, the method exits in error.
– If there is no syntaxic error in the B source file, it runs through teh Betree list.
– For each Betree:
~ It looks for the corresponding component in the list of components of the B source file (search_component)
~ If the checksum of the component is NULL (i.e. component has been modified), the method calls the decompile_betree function twice:
The first time defining the parameters of the decompiler so it will expanse the definitions and parenthisise the renamings (option for the old tools).
The second time defining the parameters of the decompiler so it will decompile the Betree identically.

– If the decompilations went well, the new checksum is stored in the component.
– An indicator is also positioned in the project manager (set_save_flag) to inform the session monitor that the checksums have been modified so it will save the project on a disk.

Atelier B differential

  • Presentation

During the functioning of Atelier B in « differential » mode, it is necessary to know for a given component the list of operation that have been modified since the last call to the proof obligation generator. The T_component::set_modified_op_list method creates this list. It Algorithm is decribed hereinafter.

Algorithm

– The input parameter is the access path to the file containing the state of the component.
– If the state file is not present,
~ The list of all the components operations is created.
~ The first element of that list is returned.

– The file is loaded: the comp_state objet of the T_component class that models the state of the component that needs to be treated is retrieved.
– The semantic Betree of the component is created.
– The component context checksums are compared:
~ For each clause different from the INITIALISATION and OPERATION clause, the checksum contained in the comp_state is compared to the one provided by the semantic Betree.
~ The same comparison is made on the machines required and/or refined by the component, knowing that the INCLUDES, EXTENDS, and INPORTS clauses are transitive.

– If a difference is found in these context checksums,
~ A list of all the components operations is created.
~ The first element of this list is returned.

– If not, for each of the components operations:
~ The checksums of the precondition and of the body of the operation contained in comp_state et those calculated on the semantic Betree are compared.
~ For each called operation, a verification is made to insure that it is defined in the same machine, then the same comparison is made.
~ The same comparison is made for the refined operation and the operations it calls.
~ The operation precondition checksums in all the component abstractions are compared.
~ In no difference is foundm
The operation is added to the list.

– The first element of this newly created list is returned, or NULL if this list is empty.