B compiler semantic phase specification 1.9
From ClearSy Tools
Note : this translation of the original .pdf documentation don't include any pictures. If you want to see them, refers to .pdf documentation
AUTHOR RESUME: This document presente specifications of semantic analysis of B Compiler phase
Versions history
ClearSy : Initial version, 03/07/2008
Chapter 1 : Introduction
The B compiler allows the analysis of a B component ASCII source file. It produces a data structure that represents the component. This data structure is a tree, called Betree 1.
During the construction of this tree, the ASCII source file is analized under different point of wiews :
- Lexical analysis, where the integrity of the lexems in the source is verified.
- Syntaxic analysis, where the conformity of the source with the languages' gramar is verified.
- Semantic analysys, where identifiers are resolved, and the data is typed by inference.
- B0 Verification, specified in [SPEC B0C NG].
This document presents the specifications of the semantic analysis phase. During this phase, two types of operations are carried out:
- Control operations, that verify that the component respect a certain number of semantic rules linked to the clauses.
- Range resolution and type inference operations, essential to the continuation of the B development process (proof obligation generation, proof, translation).
The semantic analysis therefor has a two missions in the B compiler: A policeman mission, that detects a B source conformity label, and a builder mission, that decorates the Betree with the results of its range resolutions and inference typing.
This document precisely specifies these two mission, that are carried out in sequence, in the previously stated order.
The rules used to accomplish these missions are exposed and justified in the [BBOOK] and [REF B] reference documents. THe present document takes up these requirements without justifying them.
The requirements applicable to the semantic analysis pass are referenced by an indentifier following the conventions presented in paragraph 2.3.2.
All of the requirement identifiers of this specification are reported in [REF B], where the requirement was formulated.
Error messages produced during the semantic analysis phase are implemented by means of the in-out manager of the B compilor, specified in the [CPL3] document.
Chapter 2 : Terminology & conventions used
Terminology
API "Application Program Interface": Programing interface offered by a library
Library: A library is a set of B components.
B Component: A B component designates indifferently an abstract machine, a raffinement, or an implementation.
Project Dependency graph: The project dependency graph is composed of all the components of the project, a component A is linked to a component B if and only if B is a machine required by A.
Identifier: An identifier designates the whole formed by a B data, meaning its name, its type, and its range.
Machine instanciation: An abstract machine that has formal parameters is instanciated when it is used in a component that gives effective values to the formal parameters.
Required machine: A componant A requires a machine B if and only if A sees, imports, includes, uses, or expands B.
B Module: A B module allows the imitation of an under-system : Its constitutes a part of a B project. A module designates a abstract machine and its succesive raffinements.
Operation: An operation is a service offered by a B module. The operations constitute the dynamic part of a module.
Developped operation: A developped operation is an operation whose body is given in the component.
Project: A project is composed of component that are linked by means of visibility links or importations. The components come from a dedicated development or libraries.
Prototype: The prototype of an operation, also called signature, is composed of the operations name, the list of its input parameters, and the list of its output parameters.
Scalar: Data whose type is an integer, booleen, enumerated set or abstract set element.
Enumerated value: An enumerated value is an element of an enumerated set.
Lexical conventions
Ce document donne la liste exhaustive des exigences s'appliquant au compilateur B. Chaque fois que cela est possible, la correspondance avec des documents de référence de l'Atelier-B est fournie. Pour des raisons de compacité d'écriture, les conventions suivantes seront utilisées :
Format Exemple Provenance MTC-xx MTC-101 Document [MSG TC], message xx TC-xx TC-1.2.9 Document [SPEC TC], section xx B-xx B-Header.3 Document [SPEC B0C], exigence xx
Coding convention
Coding rules
Les règles de codage présentées dans le document [DBL2] seront scrupuleusement respectées.
Coverage of requirements by the source code
Les exigences présentées dans cette spécification sont toutes repérées par un identifiant, comme par exemple CSYN 1-1 ou PROJ 3-7 Chaque portion de code couvrant une exigence doit explicitement marquer cette couverture en comportant un commentaire du format suivant : // CTRL Ref : numéro exigence Par exemple, le code qui vérifie l'exigence CSYN 1-1 doit contenir le commentaire suivant : // CTRL Ref : CSYN 1-1 Le Makefile doit posséder une entrée check qui extrait du code source les exigences couvertes (par exemple en faisant une extraction des lignes qui contiennent les lexèmes CTRL Ref :). Ainsi, en tapant make check, on pourra à tout instant vérifier la couverture des exigences de cette spécification par le code du compilateur B.
Chapter 3 : Requirements
Presentation of the software product mission
Software position in the system
La figure 3.1 page 6 présente l'architecture générale du compilateur B. L'analyseur sémantique du compilateur B est appelé après la phase d'analyse syntaxique d'un composant, afin de résoudre1 et de décorer2 le Betree qui représente ce composant. La figure 3.2 page 7 illustre la chronologie de création d'un Betree. Cette création se fait en deux étapes :
- Syntaxic analysis
Cette étape, décrite dans le document [CPL2], permet de créer un Betree syntaxique à partir d'un fichier source B sous forme ASCII.
- Semantic analysis
Cette étape permet de finaliser la construction d'un Betree. Contrairement à l'étape précédente, cette étape nécessite des données externes (i.e. autres que celles du composant analysé) pour pouvoir être effectuée. Plus précisément, si un composant M utilise des composants N1;N2; : : :Nn, alors on ne peut effectuer l'analyse sémantique de M que si les analyses sémantiques de N1;N2; : : :Nn ont toutes été effectuées avec succès. Ainsi, le compilateur B consistera à récupérer sous forme binaire les Betree sémantiques des com- posants requis, s'ils existent, avant de déclencher l'analyse sémantique du composant proprement dit.
General functions of the sotfware
L'analyseur sémantique du compilateur B a trois missions principales lors de l'analyse d'un composant B: 1. Vérifier la conformité du composant avec les règles sémantiques du langage B: exigences CSYN3, CSEM4, et PROJ5. 2. Détecter les éventuelles collisions d'identificateurs. Ces conflits sont soit des conflits implicitement liés au langage B (par exemple, si deux composants d'un projet ont le même nom), soit des conflits \cachés", provenant de choix de conception des outils de preuve qui se basent sur les résultats de l'analyse sémantique. Les exigences ECOL, présentées au Chapter II spécifient les contrôles à réaliser. 3. Résoudre les utilisations des identificateurs, en utilisant des règles de visibilité selon les exigences EHR, et ERES présentées au Chapter 11. 4. Typer les données du Betree, en utilisant des règles de typage par inférence. Vérifier la compatibilité des types utilisés dans les expressions. Les exigences TYPE6, VTYPE7, ITYPE8, LTYPE9 et LVAL10 spécifient la passe de typage du Betree
Semantic analysis dynamics
Comme illustré dans la figure 3.2 page 7, la dynamique de l'analyse sémantique d'un composant B est la suivante 11. 1. Chargement des machines requises (dans l'état de Betree syntaxique).5 2. Contrôles de conformité du composant avec les règles sémantiques du langage B. 5 Les contrôles sont effectués successivement : (a) Au niveau du composant, (b) Au niveau du projet. La partie I de ce document présente l'ensemble des règles de conformité qui sont vérifiées par l'analyseur sémantique. 5 3. Contrôles d'anticollision au niveau du projet. 5 La partie II de ce document présente l'ensemble des règles utilisées pour ces contrôles. Ces contrôles, spécifiés aux Chapters 9 et 10, sont effectués après une phase de détection des collages 5, décrite au Chapter 8. 4. Résolution des identificateurs. 5 Cette phase, présentée dans la partie III, comporte les étapes utilisées et les tables de visibilité (Chapter 6.3.1). 5. Inférence de type. 5 L'inférence se fait successivement : (a) sur les machines requises 5 (b) sur le composant 5 La partie IV du présent document est consacrée à cette étape de l'analyse sémantique.
First part : Conformity analysis
Chapter 4 : Syntaxic locals controls to a component
Introduction
Les contrôles syntaxiques au niveau d'un composant sont des contrôles simples, qui concernent principalement l'utilisation de clauses. Ces vérifications peuvent toutes être effectuées \hors contexte", c'est à dire qu'elles peuvent être effectuées localement à un composant, sans avoir besoin d'analyser les machines qu'il utilise. Ainsi, ces vérifications peuvent avoir lieu dès la fin de l'analyse syntaxique, avant même de lancer l'analyse sémantique \approfondie". Pour cette raison, ces vérifications seront effec- tuées avant la phase d'analyse sémantique, en fin de phase d'analyse syntaxique. L'avantage de cette approche est de pouvoir prévenir le plus tôt possible l'utilisateur de pro- blèmes de conception de ses composants au fur et à mesure de leur écriture, sans avoir besoin de développer un ensemble cohérent de composants pour que ces erreurs \triviales" soient détectées. D'autres contrôles de conformité, nécessitant une visibilité sur les machines requises par le com- posant, sont effectués dans un deuxième temps, au début de l'analyse sémantique du composant. Ces contrôles sont présentés au Chapter 5. Dans ce Chapitre, les contrôles suivants sont présentés : - Restrictions d'utilisation : - Restrictions d'utilisation de clauses (section 4.2.1) : certaines clauses ne sont pas au- torisées dans tous les types de composant, par exemple la clause REFINES ne peut pas être utilisée dans une machine abstraite. - Restrictions d'utilisation d'expressions (section 4.2.2) : certaines expressions comme $0 ne peuvent pas être utilisées dans tous les contextes. - Restrictions d'utilisation de substitutions (section 4.2.3) : certaines substitutions ne sont pas autorisées dans tous les types de composant, par exemple la substitution VAR ne peut pas être utilisée dans une machine abstraite. - Vérification de présence de clauses obligatoires (section 4.3). - Détection d'utilisations abusives (section 4.4). - Vérification d'unicité des clauses (section 4.5). - Contrôles sur les prédicats (section 4.6). - Contrôles sur les expressions (section 4.7).
/*
* * GROS TROU * * */
Restrictions on use predicate to B0
Dans les implantations, les prédicats doivent être des conditions. Une condition est un prédicat traduisible dans les langages de programmation classiques. Les prédicats peuvent être classés en deux catégories : - Les prédicats qui ne peuvent dans aucun cas être des conditions. Décrits au paragraphe 4.6.1, ces prédicats sont interdits en implémentation. - Les prédicats qui peuvent, sous certaines restrictions, être des conditions. Le paragraphe 4.6.2 donne la liste de ces prédicats, avec, pour chacun d'entre eux, les contrôles à effectuer pour savoir s'il s'agit d'une condition.
Predicates who can be conditions
Les contrôles CSYN 8-1 à 8-5 précisent les conditions nécessaires et su±santes pour que les prédicats listés soient des \conditions". Remarque : La notion de terme simple est précisée au paragraphe 4.7.2.
Restrictions on use of expressions to B0
Dans les implantations, les expressions doivent être des termes. Un terme est une expression traduisible dans les langages de programmation classiques. Les expressions peuvent être classées en deux catégories : - Les expressions qui ne peuvent dans aucun cas être des termes. Décrites au paragraphe4.7.1, ces expressions sont interdites en implémentation. - Les prédicats qui peuvent, sous certaines restrictions, être des termes. Les paragraphes 4.7.1, 4.7.2 à 4.7.6 donnent la liste de ces expressions, avec, pour chacune d'entre elles, les contrôles éventuels à effectuer pour savoir s'il s'agit d'un terme.
Simples terms
Les termes simples sont autorisés en implémentation. Un certain nombre de constructions (condi- tions, . . . ) ne sont valides en B0 que si les expressions qu'elles contiennent sont des termes simples. C'est pour cela que la notion de terme simple est précisée ici. Un terme simple ne peut être que l'une des quatre constructions suivantes : 1. CSYN 10-1 : Un identificateur (éventuellement renommé) 2. CSYN 10-2 : Un entier littéral 3. CSYN 10-3 : Un booléen littéral 4. CSYN 10-4 : Un accès à un champ de record
Terms
Les termes sont des expressions autorisées en implémentation sous certaines conditions, expri- mées dans le tableau ci-après. Le tableau ne présente pas les termes simples, qui sont décrits au paragraphe précédent, et qui sont toujours autorisés en implémentation.
Arithmetic contribution
La liste exhaustive suivante définit les expressions arithmétiques : - CSYN 12-1 : Un entier littéral - CSYN 12-2 : Un identificateur (éventuellement renommé) - CSYN 12-3 : Une somme, une différence, un produit ou une division de deux expressions arithmétiques - CSYN 12-4 : L'opposé d'une expression arithmétique - CSYN 12-5 : Le modulo de deux expressions arithmétiques - CSYN 12-6 : L'élévation à la puissance de deux expressions arithmétiques - CSYN 12-7 : Le successeur ou le prédécesseur d'une expression arithmétique
Board expressions
La liste exhaustive suivante définit les expressions de tableau : - CSYN 13-1 : Un identificateur - CSYN 13-2 : Une liste de \maplets" entre crochets. Un \maplet" est, dans ce contexte, un n-uplet dont l'indice est un terme simple, et la valeur un terme. - CSYN 13-3 : Un produit cartésien d'une plage par un singleton. Une plage est, dans ce contexte, un intervalle B0 ou un identificateur. Remarque : CSYN 13-3 est plus contraignante que [REF B] 1, mais [REF B] sera corrigé pour être en accord avec ce document.
B0 intervals
La liste exhaustive suivante définit les intervalles B0 : - CSYN 14-1 : Un intervalle explicite dont les deux bornes sont des expressions arithmétiques - CSYN 14-2 : NAT, NAT1 ou INT
Chapter 5 : Semantic controls
Introduction
Les contrôles présentés dans ce Chapter sont des contrôles de conformité de niveau sémantique. Ils nécessitent que tous les composants utilisés par le composant en cours d'analyse aient subi avec succès l'étape d'analyse sémantique. Ces contrôles ont lieu dès le début de l'analyse sémantique d'un composant. Au sein du cycle complet de compilation d'un composant B, ils suivent chronologiquement les contrôles de confor- mité de niveau syntaxique décrits au Chapter 4.
Controls on project
Introduction
Les contrôles présentés dans ce Chapter sont des contrôles d'intégrité au niveau d'un projet. Ils nécessitent des informations sur le composant en cours d'analyse, sur ses abstractions, et sur les machines requises. Au sein du cycle complet de compilation d'un composant B, ils suivent chronologiquement les contrôles de conformité de niveau sémantique décrits au Chapter 5. Ces contrôles sont de trois types : - Les vérifications locales à un composant étudient l'emploi des machines requises. Elles sont décrites au paragraphe 5.3.2. - Les vérifications locales à un module sont relatives au composant et à ses abstractions. Elles sont décrites au paragraphe 5.3.3. - Les vérifications globales au projet sont effectuées
Global verifications on project
Les vérifications globales au projet sont des vérifications qui ne peuvent pas être effectuées unitairement sur les composants du projet. Elles ne sont donc pas effectuées par le compilateur B lors de la compilation unitaire, mais par un éditeur de liens, intégré au compilateur B, qui travaille sur un projet complet. Ces contrôles sont précisés et justifiés dans le document [NOTE5].
Second part : Anti-collision controls
Chapter 6 : Introduction
Environments
Les contrôles d'anticollision vérifient qu'il n'y a pas d'ambiguijté au sein des identificateurs utilisés dans un projet B. Les identificateurs étant définis par leur nom, il y a ambiguijté lorsque deux identificateurs représentant des entités distinctes sont présents dans un même environnement. La figure 6.1 illustre la notion d'environnement dans un composant B. Plus formellement, lors de l'analyse d'un composant M qui requiert les composants R1;R2; : : :Rn, les environnementssuivants sont à considérer : - L'environnement global, composé des identificateurs exportés par M et R1;R2; : : :Rn. Chacun de ces composants exporte les identificateurs suivants dans cet environnement : ses opérations, ses constantes, ses variables, ses ensembles et ses valeurs énumérées. Si l'un des composants Ri est utilisé avec renommage, c'est à dire qu'il est de la forme instance:composant, alors ses variables sont exportées, préfixées par \instance.". Il en est de même pour ses opérations, les autres identificateurs étant exportés tels quels. - L'environnement de composant, local à chaque composant, constitué de l'environnement global, enrichi des paramètres formels du composant. - L'environnement de bloc, local à chaque substitution et prédicat, et plus généralement à chaque bloc qui introduit des identificateurs, constitué de l'environnement de composant si le bloc n'est pas contenu dans un autre bloc, ou de l'environnement du bloc de niveau supérieur qui contient le bloc dans le cas contraire, augmenté des identificateurs locaux. Les contrôles de collision prennent en compte les visibilités des données. En effet, le langage B définit, pour chaque type de donnée, des règles de visibilité qui définissent la fa»con dont elle peut être utilisée au sein du composant lui-même ou d'un composant utilisant ce composant. La section suivante définit les tables de visibilité utilisées par le compilateur B pour modéliser les portées des données.
Differences with "Type Checker" of the first string
L'outil \Type Checker" de la première cha^³ne de l'Atelier B a un comportement qui diffère de celui du compilateur B pour les points suivants : - Le \Type Checker" préfixe (à tort) les constantes abstraites du nom d'instance en cas de renommage. - Le \Type Checker" ne préfixe pas (à tort) les paramètres formels du nom d'instance en cas de renommage.
Modelisations of visibility tables
Presentation
Le document [REF B] définit, dans son annexe C, les tables de visibilité entre deux composants C1 et C2, définissant pour chaque constituant de C2 les modes d'accès applicables dans les clauses de C1. Ces tables sont modélisées dans le compilateur B, et sont utilisées au cours de la phase de résolution des identificateurs. En effet, lors de la résolution de chaque identificateur, il faut s'assurer que la définition que l'on trouve est \visible", c'est à dire que l'utilisation faite de l'identificateur est légale. Le paragraphe suivant présente la modélisation des tables de visibilité au sein du compilateur B.
Modelisation
La modélisation des tables de visibilité fait intervenir les notions suivantes : - le type ¿ de l'entité accédée, modélisé au moyen du type énuméré T_access_entity_type : paramètre formel, ensemble abstrait, . . . - la localisation ¢ de cette entité, modélisé au moyen du type énuméré T_access_entity_ location : machine vue, abstraction, . . . - le contexte à de l'identificateur à résoudre, modélisé au moyen du type énuméré T_access_ from_context : clause CONSTRAINTS, prédicat de ASSERT, substitution, . . . . - le type ± de l'autorisation d'accès, modélisé au moyen du type énuméré T_access_ authorisation : autorisation de lecture, d'écriture, pas d'autorisation, . . . Alors les tables permettent de définir une fonction telle que ± = (¿;¢; Ã) soit l'autorisation d'accès de la définition potentielle de l'entité accédée. Les tables sont initialisées au cours de la phase d'initialisation du compilateur B. Elles utilisent les structures de données suivantes : Entités accédées Le type énuméré T_access_entity_type permet de modéliser les types des entités pouvant être accédées depuis un source B.
/*
* * TROu * */
Visibility tables
La paramétrage dit du \SEES étendu" est possible. La section A.2 page 95 donne la marche à suivre pour utiliser ce mode des tables de visibilité. Ce paramétrage permet d'accéder aux variables concrètes et abstraites des machines vues depuis les clauses INVARIANT et ASSERTIONS des composants B. Les tables de visibilité ne sont pas fournies dans ce document. Leur référence est fournie dans le document [REF B], qui sert de spécification pour ces tables.
Chronology of controls
Ces contrôles doivent avoir lieu avant les phases de résolution des identificateurs, puis de typage, afin d'être s^ur que l'on peut référencer de fa»con unique chaque identificateur par son nom. La plupart des conflits potentiels sont intimement liés à la sémantique du langage B, et plus précisément aux portées des structures de données du langage. Ces conflits sont décrits dans le Chapter 9. D'autres conflits potentiels sont d^us à la génération des obligations de preuve en aval du compilateur B. Ces conflits \cachés" sont présentés au Chapter 10. La détection de ces deux types de conflits nécessite au préalable l'héritage de l'environnement de l'abstraction et des machines requises, puis la détection des collages par homonymie des structures de données. Ces deux étapes sont décrites respectivement aux Chapters 7 et 8. Les exigences suivantes sont définies pour cette passe : - EHER: héritage de l'environnement de l'abstraction et des machines requises. - EDET 1 : détection des collages. - EDET 2 : détection des conflits liés à la sémantique du langage. - EDET 3 : détection des conflits cachés.
Chapter 7 : Heritage
Un composant hérite, implicitement ou explicitement, d'un certain nombre d'opérations et de structures de données de son abstraction et de machines requises. Ces éléments hérités doivent être intégrés au sein de l'environnement du composant en cours d'analyse, car ils influent non seulement sur la phase de résolution des identificateurs présentée au Chapter 12, mais aussi sur la phase de détection des collages décrite au Chapter 8. Ce Chapter spécifie quels sont les éléments qui peuvent être hérités, et précise le contexte éven- tuellement nécessaire pour qu'il y ait héritage.
Concrete variables & constantes
EHER 1 : D'après [REF B], un composant hérite des variables concrètes et des constantes concrètes de son abstraction.
Abstract variables & constants
EHER 2 : D'après [REF B], si un composant ne ra±ne pas une variable (ou constante) abstraite de son abstraction, alors cette variable (ou constante) ne fait pas partie de la liste des variables (ou constantes) abstraites du composant : elle \dispara^³t". Autrement dit, un composant hérite d'une variable (respectivement constante) abstraite de son abstraction si et seulement si sa déclaration est répétée dans la clause ABSTRACT_VARIABLES (respectivement ABSTRACT_CONSTANTS) de ce composant.
Included machines
EHER 3 : D'après [REF B], un composant hérite des ensembles (abstraits et énuméres), des constantes, des variables des machines incluses. Par contre, les opérations ne sont pas héritées, sauf si le composant qui inclut le demande explicitement au moyen de la clause PROMOTES. La clause INCLUDES étant transitive, le composant hérite des données provenant des composants inclus et étendus par les composants qu'il inclut.
Machines extended
EHER 4 : D'après [REF B], un composant hérite des ensembles (abstraits et énumérés), des constantes, des variables et des opérations des machines étendues. La clause EXTENDS étant transitive, le composant hérite des données provenant des composants inclus et étendues par les composants qu'il étend.
Settings formal operation
EHER 5 : D'après [REF B], une opération présente dans un ra±nement ou une implémentation n'a pas besoin de typer ses paramètres formels car ceux-ci héritent du type qui leur a été attribué dans la machine abstraite. Ainsi, les éventuels typages fournis dans les ra±nements et les implémentations doivent êtres compatibles avec ceux spécifiées dans la machine abstraite.
Chapter 8 : Detection of collages by homonymy
Example
On parle de collage par homonymie lorsque qu'une structure de données B est implicite- ment implémentée par une structure de données compatible 1, de même nom, qui provient d'une machine requise. Dans l'exemple de la figure 8.1, la machine abstraite M définit une variable abstraite x. Son implémentation M_i n'implémente pas x. Par contre, M_i importe la machine N, qui définit la variable concrète x. On dit que la variable abstraite x de M_i est collée par homonymie avec la variable concrète x de N. Autrement dit, M_i délègue la responsabilité de l'implantation de x à N.
Definition
General principle
La notion de collage est propre aux ra±nements et aux implémentations. Les structures de données qui peuvent être collées sont : 1. les variables abstraites et concrètes, 2. les constantes abstraites et concrètes, 3. les ensembles abstraits, 4. les ensembles énumérés. Dans le cas général, il y a collage par homonymie lorsqu'une entité qui appartient à ces structures de données n'est pas implantée dans le composant, et que de plus ce composant importe 2 un composant qui définit une structure de données compatible et de même nom. En outre, il faut que les types des deux identificateurs soient identiques.
Others cases of collage
- Les constantes et les ensembles peuvent également être collés si le composant voit une structure de données compatible et de même nom. - Une constante (respectivement une variable) abstraite peut être collée par une constante (respectivement une variable) concrète dans un ra±nement ou une implémentation, si la constante (respectivement la variable) abstraite est définie dans l'abstraction de ce com- posant.
Compatibility
Le tableau ci-après donne, pour chaque structure de données du langage, les structures de données compatibles pouvant être utilisées dans un collage par homonymie.
Names identifiers
Comme nous l'avons vu, pour coller un identificateur avec un identificateur x provenant d'un composant renommé ins, il faut donner le nom x.ins à l'identificateur \à coller". Il est donc possible de créer des variables dont le nom comporte un ou plusieurs points. Par contre, il est interdit de créer artificiellement de tels identificateurs. La contrainte COLL 2, présentée dans la section suivante, exprime cette interdiction. /*
* * TROUUUUUUUUUUUUUU * */
Modelisation
La classe T_ident est enrichie d'un champ ref_glued et d'un champ implemented_by, de type T_ident*. Pour les identificateurs collés, le champ référence l'identificateur avec lequel le collage a lieu. Pour les identificateurs non collés, ce champ vaut NULL. En implantation, le champ implemented_by référence l'identificateur homonyme d'une machine vue, importée ou étendue. Si le champ est à NULL, alors l'ident est implanté en propre sinon l'identificateur est implanté par homonymie et le champ référence l'identificateur qui l'implé- mente à l'extérieur. Dans une spécification ou un ra±nement, le champ n'a pas de sens et est à NULL.
Detection principle
Algorithm
La détection se fait en parcourant les ensembles abstraits et énumérés, les constantes abstraites et les variables abstraites de l'abstraction du composant qui ne sont pas implantés dans ce composant. Pour chacun de ces identificateurs, le compilateur recherche dans les machines importées, in- cluses, étendues et éventuellement vues un identificateur de même nom. Si un tel identificateur est trouvé, la compatibilité des deux identificateurs est vérifiée. Si elles sont compatibles, le champ ref_glued de l'identificateur \collé" est mis à jour ainsi que le champ implemented_by en implantation. Sinon, le champ est laissé à NULL. Pour chaque identificateur, la recherche s'arrête dès qu'un collage est trouvé. Si plusieurs collages sont possibles, il y a un conflit, qui sera détecté lors du contrôle d'anticollision, présenté au Chapitre 9.
Particular case of a renamed machine
Si l'une des machines parcourues est renommée, et que l'identificateur en cours d'analyse est une variable (abstraite ou concrète), alors le préfixe de renommage est pris en compte dans la recherche. Par exemple, si la machine M définit une variable abstraite instance.var, alors son implémen- tation peut la coller par homonymie en important l'instance instance.N d'une machine N qui définit une variable var.
Chapter 9 : Conflict linked to semantic of B langage
Introduction
Ce Chapter présente la liste des conflits liés à la sémantique du langage B qui doivent être détectés par l'analyse sémantique Les contrôles présentés dans ce Chapter proviennent du document [REF B]. Cette section présente la méthode générale de détection des conflits. Le paragraphe 9.2 précise ensuite l'implication de l'utilisation d'instances renommées sur la détections des conflits.
Impact on renaming the detection of conflicts
Si une machine M est utilisée avec renommage, c'est à dire qu'un composant utilise une instance i.M, alors les variables, les opérations et les paramètres formels de i.M sont accessibles depuis le composant qui utilise en préfixant leur nom par \i." : ainsi, on désigne un espace de données propre à l'instance considérée. Par contre, les ensembles abstraits et énumérés et les valeurs énumérées du composant sont vues depuis le composant qui importe avec leur nom usuel : ainsi, on désigne un espace de données commun à toutes les instances de M.
Detection of conflict for an abstract machine
Soit M la machine abstraite analysée. Le contrôle d'anticollision consiste à créer la liste L, union des listes Lmch, Lsees, Linc et Luses décrites ci-après, puis à vérifier que les noms présents dans L sont deux à deux distincts. - Soit Lmch la liste composée (exigence ELMCH): 1. du nom de M, 2. des noms des paramètres de M, 3. des noms des ensembles abstraits et énumérés de M, 4. des noms des valeurs énumérées définies dans M, 5. des noms des constantes de M, 6. des noms des variables de M, 7. des noms des opérations de M - Soit Lsees la liste composée, pour chaque machine N vue(exigence ELSEES), 1. du nom de N, 2. des noms des ensembles abstraits et énumérés de N, 3. des noms des valeurs énumérés de N, 4. des noms des constantes de N, 5. des noms des variables de N, 6. des noms opérations de N Les noms des constantes, des ensembles et des valeurs énumérées ne sont insérés qu'une seule fois par composant, si le composant est référencé plusieurs fois. Par contre, les noms des variables et des opérations sont préfixés par le nom d'instance en cas de renommage. - Soit Linc la liste composée, pour chaque machine N incluse ou étendue (exigence ELINC), 1. du nom de N, 2. des noms des ensembles abstraits et énumérés de N, 3. des des valeurs énumérées de N, 4. des noms des constantes de N, 5. des noms des variables de N, 6. des noms des opérations de N Les noms des constantes, des ensembles et des valeurs énumérées ne sont insérés qu'une seule fois par composant, si le composant est référencé plusieurs fois. Par contre, les noms des variables et des opérations sont préfixés par le nom d'instance en cas de renommage. - Soit Luses la liste composée, pour chaque machine N utilisée (exigence ELUSES), 1. du nom de N, 2. des noms des paramètres de N, 3. des noms des ensembles abstraits et énumérés de N, 4. des noms des valeurs énumérées de N, 5. des noms des constantes de N, 6. des noms des variables de N Les noms des constantes, des ensembles et des valeurs énumérées ne sont insérés qu'une seule fois par composant, si le composant est référencé plusieurs fois. Par contre, les noms des variables, des opérations et des paramètres formels sont préfixés par le nom d'instance en cas de renommage.
Detection of conflict for a refinement
Soit M0 le ra±nement analysé, et soit M sa machine abstraite. Le contrôle d'anticollision consiste à créer la liste L, union des listes Lraf, Lsees et Linc décrites ci-après, puis à vérifier que les noms présents dans L sont deux à deux distincts. - Soit Lraf la liste composée (exigence ELRAF): 1. du nom de M, 2. des noms des paramètres de M0, 3. des noms des ensembles abstraits et énumérés de M0, 4. des noms des valeurs énumérées définies dans M0, 5. des noms des constantes de M0, 6. des noms des variables de M0, 7. des noms des opérations propres de M0 Les opérations propres à un ra±nement, sont les opérations de la spécification, moins les opérations qui sont promues dans le ra±nement. - Soit Lsees la liste composée, pour chaque machine N vue (exigence ELSEES), 1. du nom de N, 2. des noms des ensembles abstraits et énumérés de N, 3. des noms des valeurs énumérées de N, 4. des noms des constantes de N, 5. des noms des variables de N, 6. des noms opérations de N Les noms des constantes, des ensembles et des valeurs énumérées ne sont insérés qu'une seule fois par composant, si le composant est référencé plusieurs fois. Par contre, les noms des variables et des opérations sont préfixés par le nom d'instance en cas de renommage. - Soit Linc la liste composée, pour chaque machine N incluse ou étendue (exigence ELINC), 1. du nom de N, 2. des noms des ensembles abstraits et énumérés de N, 3. des des valeurs énumérées de N, 4. des noms des constantes de N, 5. des noms des variables de N, 6. des noms des opérations de N Les noms des constantes, des ensembles et des valeurs énumérées ne sont insérés qu'une seule fois par composant, si le composant est référencé plusieurs fois. Par contre, les noms des variables et des opérations sont préfixés par le nom d'instance en cas de renommage.
Conflicts detection for an implementation
Soit M0 l'implémentation analysée, et soit M sa machine abstraite. Le contrôle d'anticollision consiste à créer la liste L, union des listes Limpl, L_impo et Lsees décrites ci-après, puis à vérifier que les noms présents dans L sont deux à deux distincts. - Soit Limpl la liste composée (exigence ELIMP): 1. du nom de M, 2. des noms des paramètres de M0, 3. des noms des ensembles abstraits de M0, sauf ceux qui sont valués par homonymie, 4. des noms des ensembles énumérés et des valeurs énumérées de M0, sauf pour les ensembles énumérés homonymes à un ensemble énuméré d'une machine requise, 5. des noms des constantes concrètes de M0, sauf celles qui sont valuées par homonymie, 6. des noms des variables concrètes de M0, sauf celles qui sont valuées par homonymie, 7. des noms des opérations développées de M0, 8. des noms des constantes abstraites et des variables abstraites de l'abstraction de M0 qui disparaissent dans M0 Les noms des constantes, des ensembles et des valeurs énumérées ne sont insérés qu'une seule fois par composant, si le composant est référencé plusieurs fois. Par contre, les noms des variables, des opérations et des paramètres formels sont préfixés par le nom d'instance en cas de renommage. - Soit Limpo la liste composée, pour chaque machine N importée(exigence ELIMPORTS), 1. du nom de N, 2. des noms des ensembles abstraits et énumérés de N, 3. des valeurs énumérées de N, 4. des noms des constantes de N, 5. des noms des variables de N, 6. des noms des opérations de N Les noms des constantes, des ensembles et des valeurs énumérées ne sont insérés qu'une seule fois par composant, si le composant est référencé plusieurs fois. Par contre, les noms des variables et des opérations sont préfixés par le nom d'instance en cas de renommage. - Soit Lsees la liste composée, pour chaque machine N vue (exigence ELSEES), 1. du nom de N, 2. des noms des ensembles abstraits et énumérés de N, 3. des noms des valeurs énumérées de N, 4. des noms des constantes de N, 5. des noms des variables de N, 6. des noms opérations de N Les noms des constantes, des ensembles et des valeurs énumérées ne sont insérés qu'une seule fois par composant, si le composant est référencé plusieurs fois. Par contre, les noms des variables et des opérations sont préfixés par le nom d'instance en cas de renommage.
Specification product message in the event of collision
La fonction double_identifier_error est appelée en cas de collision. Elle utilise les messages formatés E_IDENT_CLASH et E_IDENT_CLASH_OTHER_LOCATION pour préciser le nom, la nature et la localisation des deux identificateurs qui provoquent la collision. Exemple de messages produits : CC.mch:20:5: Definition of identifier "VAR_CC" as a concrete constant clashes with previous definition as a concrete constant AA.mch:20:5: Location of conflicting definition BB.mch:17:5: Definition of identifier "VAR_BB" as a concrete variable clashes with previous definition as a concrete variable
Chapter 10 : Hidden conflicts
Introduction
Les conflits cachés résultent de choix de conception des outils de preuve en aval du compilateur B: générateur d'obligations de preuve et prouveur. Les documents [NOTE2] et [SPEC TC] en présentent une première spécification, qui s'est avérée incomplète. Les conflits cachés ne sont effectués que sur demande explicite de l'utilisateur (option -p sur la ligne de commande). Ainsi, le compilateur peut remplacer complètement le Type Checker, qui effectuait, partiellement, ce travail de vérification dans les anciennes versions de l'Atelier B.
Anti-collision controls
Soient Mn le composant analysé, Mi (avec i 2 [1::n ¡ 1]) ses abstractions successives, et M0 sa spécification. Le graphe local de Mn est constitué des composants suivants : - le composant Mn, - les abstractions Mi (avec i 2 [0::n ¡ 1]) de Mn, - les instances des machines requises par l'un des composants du graphe local.
Justifications
Lors de la construction d'un obligation de preuve, des identificateurs venant de composants différents sont mis au même niveau. Il est donc possible d'avoir des conflits de nom entre deux données différentes. Cas d'un identificateur issu d'une des abstractions de Mn ou d'une des machines incluses dans une abstraction de Mn La figure 10.1 page 48 présente un exemple de graphe local avec des abstractions. Les invariants des machines Mi et I sont en hypothèse des obligations de preuve des opérations de la machine Mn. Or les variables, les constantes, les ensembles, les éléments énumérés et les paramètres formels de machine peuvent appara^³tre dans l'invariant d'un composant. Donc tous ces identificateurs définis dans Mi ou I (sauf ses paramètres formels) peuvent générer un conflit caché. Les paramètres formels de I sont remplacés par leur valeur effective avant la construction de l'obligation de preuve, ce qui explique qu'ils ne peuvent pas générer de conflit. Cas d'un identificateur issu d'une machine requise par Mn ou Mn¡1 La figure 10.2 page 48 présente un exemple de graphe local avec des machines requises. Cet exemple est possible quels que soient les liens, si les opérations op2 et op3 sont des opérations de consultation. Lors de la construction de l'obligation de preuve de op, les corps des opérations sont expansés, c'est-à-dire que l'appel à op2 est remplacé par le corps de op2, dans lequel on aura remplacé l'appel de op3 par son corps. Donc toutes les données consultées par op3 peuvent appara^³tre dans l'obligation de preuve. Or op3 peut accéder aux variables, constantes, ensembles, éléments énumérés et paramètres formels de machine de J. Donc tous ces identificateurs peuvent générer un conflit caché, sauf les paramètres formels de J si elle est une machine incluse puisque dans les obligations de preuve c'est leur valeur effective qui appara^³t. On peut étendre l'exemple à toutes les machines transitivement requises par Mn. On peut également étendre l'exemple aux machines requises par Mn¡1. En effet le corps de l'opération de Mn¡1 est utilisé dans l'obligation de preuve de l'opération de Mn¡1.
Cas d'une machine vue ou utilisée par une abstraction de Mn¡1 La figure 10.3 page 49 présente un exemple de graphe local avec un mélange de liens REFINES et de liens SEES. Dans ce cas, seuls les constantes, les ensembles et les éléments d'énumérés de S, T et L peuvent appara^³tre dans les obligations de preuve, car ils peuvent être dans l'invariant de Mi ou Mj . Ce n'est pas le cas des paramètres formels, ni des variables (sauf si le paramétrage dit du \SEES étendu" est utilisé). Mais dans un souci de simplification, il a été décidé de ne pas traiter ce cas différemment des autres : des conflits seront également levés pour les variables et les paramètres formels de S, T et L. Identificateurs utilisés lors de la construction des obligation de preuve Les conflits cachés doivent aussi tenir compte des identificateurs utilisés lors de la construction des obligations des preuve, même s'ils n'apparaissent pas dans celles-ci. Il s'agit des noms des composants Mn et Mn¡1, et des noms des opérations de la spécification M0.
Controls speifications
Considérons la liste constituée : 1. pour chaque composant C du graphe local de Mn : (a) des noms des ensembles de C, (b) des noms des valeurs énumérées de C, (c) des noms des constantes de C, (d) des noms des variables de C, (e) des noms des paramètres formels de la machine C s'il s'agit d'une machine vue ou utilisée, 2. des noms des paramètres formels de machine de Mn, 3. des identificateurs Mn et Mn¡1, 4. des noms des opérations (propres ou promues) de M0, 5. des noms des paramètres formels de ces opérations, 6. des noms des opérations (propres ou promues) des machines vues par Mn si le paramétrage dit du \SEES étendu" est utilisé, 7. des noms des paramètres formels de ces opérations si le paramétrage dit du \SEES étendu" est utilisé. Les noms des variables et des opérations sont préfixés par le nom d'instance en cas de renommage mais sans utiliser le point de séparation. Le contrôle d'anticollision consiste à vérifier que les éléments de cette liste sont deux à deux distincts. Si deux identificateurs sont identiques, plusieurs cas sont à envisager : - Le conflit est d^u à la suppression des points de séparation du renommage (et avec les points il n'y aurait pas de conflit) : il y a bien un conflit. - Les deux identificateurs sont des variables, des opérations ou des paramètres formels de machines, et sont définis dans la même instance de machine : il n'y a pas de conflit. - Les deux identificateurs sont des constantes, des ensembles ou des valeurs énumérées, et sont définis dans la même machine : il n'y a pas de conflit. - Les deux identificateurs sont des paramètres formels d'opérations différentes : il n'y a pas de conflit. - Les deux identificateurs représentent la même donnée selon les règles d'homonymie du langage B: il n'y a pas de conflit. - Dans tous les autres cas : il y a bien un conflit. Remarque : Si deux identificateurs vérifient à la fois les conditions du premier cas (suppression des points de renommage), et celles d'un autre cas, il y a bien un conflit caché. Cette spécification des conflits cachés correspond à la cha^³ne de preuve \type checker + généra- teur d'obligations de preuve" telle qu'on la trouve dans l'Atelier B V3.6. Elle devra être modifiée lors du passage à la cha^³ne de preuve \générateur de forme normale + générateur d'obligations de preuve" telle qu'on la trouvera dans l'Atelier B V4.0. Ainsi dans cette cha^³ne les paramètres formels de machine sont préfixés par le nom d'instance en cas de renommage.
Keywords languages and tools used in the string of evidence
L'implémentation de la détection des conflits cachés doit également prendre en compte la détec- tion d'utilisation dans les sources B de mots-clés du Kernel. Il faut également détecter les conflits avec les mots-clés des langages et logiciels utilisés dans la cha^³ne de preuve : - Identificateurs réservés du Prouveur : - FORWARD - FORWARDTHEORIES - NORMAL - NORMALTHEORIES - PROOFLEVEL - PROOFMETHOD - SET - SETSPE - THEORIES - Identificateurs réservés du GOP/Animateur : - finite - infinite - choice" - plus - minus - multiply - divide - SET - Identificateurs réservés du Kernel : - ARI - CATL - DED - DEF - END - FLAT - GEN - HYP - IS - LMAP - MAP - MODR - NEWV - RES - REV - RULE - SHELL - SUB - THEORY - WRITE - bUpident - band - bappend - bcall - bcall1 - bcall2 - bcatl - bclean - bclose - bcompile - bconnect - bcrel - bcrelr - bcrer - bctrule - bdef1 - bdef2 - bdump - berv - bfalse - bfwd - bget - bgethyp - bgetresult - bgoal - bguard - bhalt - bident - binhyp - blemma - blen - blenf - blent - blident - bload - blvar - bmark - bmatch - bmodr - bnewv - bnlmap - bnmap - bnot - bnum - bpattern - bpop - bprintf - bproved - breade - breadf - brecompact - bresetcomp - bresult - brev - brule - bsearch - bsetmode - bshell - bslmap - bsmap - bsparemem - bsrv - bstatistics - bstring - bsubfrm - btest - bunproved - bvrb - bwritef - bwritem - trace
Third part : Identifier resolving
Chapter 11 : Presentation
Introduction
Comme nous l'avons vu au Chapter 3, l'analyse sémantique comporte une passe de résolution des identificateurs, au cours de laquelle on recherche les définitions de tous les identificateurs référencés dans le source B. Ce Chapter présente la modélisation utilisée dans le compilateur B pour représenter les identi- ficateurs résolus.
Example
Considérons l'exemple présenté dans la figure 11.1 de la page 58. Dans cet exemple, on représente les instances de T_ident utilisées dans les modélisations des composants AA, AA_1 (qui implémente AA) et BB (qui est importé par AA_1).
Identifier declaration
Les instances de T_ident utilisées dans la modélisation des déclarations d'identificateurs présents dans les clauses CONCRETE_VARIABLES, CONCRETE_CONSTANTS, ABSTRACT_VARIABLES, . . . sont classés par nature dès l'analyse sémantique. En effet, leur champ ident_type possède une valeur qui permet de retrouver leur nature 1. Ainsi, l'instance de T_ident utilisée pour modéliser la déclaration de abs_var dans AA a un champ ident_type qui vaut ITYPE_ABSTRACT_VARIABLE. De même, l'instance de T_ident uti- lisée pour modéliser la déclaration de init dans BB a un champ ident_type qui vaut ITYPE_ CONCRETE_VARIABLE.
Identifiers utilisation
Presentation
Les instances de T_ident utilisées pour modéliser les parties de source B oµu les identificateurs sont utilisés 2 ont, au terme de la phase d'analyse syntaxique, un champ ident_type qui vaut ITYPE_UNKNOWN. Ces identificateurs sont alors référencés comme des identificateurs à résoudre : il faut, au cours de la phase d'analyse sémantique, localiser les définitions des identificateurs qu'ils représentent. Par exemple, dans la clause INVARIANT de l'implémentation AA_1, il y a deux identificateurs à résoudre : conc_var et abs_var. La résolution de conc_var doit référencer sa définition au sein de la clause CONCRETE_VARIABLES de AA_1, et la résolution de abs_var doit référencer sa définition au sein de la clause CONCRETE_VARIABLES de la machine abstraite AA. Le Chapter 12 précise les modalités de résolution des identificateurs. Le paragraphe 11.4.2 ci- après présente tout d'abord la modélisation employée dans le Betree pour représenter la résolu- tion des identificateurs.
Modelisation
Les instances de la classe T_ident possèdent un champ def, de type T_ident *, qui est mis à jour lors de l'analyse sémantique pour tous les identificateurs pour lesquels ident_type vaut ITYPE_UNKNOWN. Ainsi, la référence sur la définition de l'identificateur est stockée dans le champ def, et l'identi- ficateur est dit résolu. Si la définition n'est pas trouvée, l'identificateur n'est pas résolu, et la valeur du champ vaut NULL. A la fin de la passe de résolution, tous les identificateurs doivent être résolus, faute de quoi l'analyse sémantique ne peut continuer (en particulier, l'inférence de type ne peut pas avoir lieu). Les exigences suivantes sont applicables à la passe de résolution de l'analyse sémantique : - ERES : résoudre tous les identificateurs du Betree. - ECOR: corriger le Betree.
Chapter 12 : Identifiers resolving
Introduction
Comme nous l'avons vu au Chapter 11, l'analyse sémantique comporte une passe de résolution des identificateurs, au cours de laquelle on recherche les définitions de tous les identificateurs référencés dans le source B. Au cours de cette recherche, il faut vérifier que les identificateurs référencés sont effectivement visibles par le composant qui les mentionne, en utilisant les notions présentées au paragraphe 6.3 page 30. Ce Chapter présente l'algorithme générique de résolution des identificateurs.
Resolution algorithm
Presentation
On souhaite résoudre un identificateur ident, par exemple dans le code B suivant OPERATIONS xx <-- op = BEGIN VAR ident IN ident := 1
Search algorithm
La recherche se fait en \remontant" progressivement dans le Betree, au moyen des méthodes get_father()1, afin de respecter la sémantique de blocs du B. Lors de la résolution de ident dans la substitution ident := 1, la méthode get_father() per- met d'atteindre successivement la substitution affectation, la substitution VAR .. IN, l'opération op puis le composant.
Pour chaque élément atteint au moyen de la méthode, il faut regarder s'il définit l'identificateur recherché. Si c'est le cas, il faut tester la visibilité de cette définition (ce test est décrit au paragraphe suivant). Si l'identificateur n'est pas visible, la recherche continue. Sinon, il faut \remonter" au niveau supérieur. Si l'identificateur n'est pas trouvé dans le com- posant en cours d'analyse, il faut analyser ses machines requises, en notant que : - EREN 1: Les variables, les opérations et les paramètres issus de machines instanciées, doivent être utilisés avec le préfixe de renommage, dans le cas d'un instanciation avec renommage et sans préfixe dans le cas d'instance sans renommage. - EREN 2: Les constantes ne doivent pas êtres préfixées. - EREN 3: Dans une machine abstraite, les opérations déclarées dans la clause opération ne doivent pas être renommées. - Seule les clauses INCLUDES et EXTENDS sont transitives, c'est à dire que l'analyse ne se propage pas au machines requises des machines requises, sauf pour le cas particulier des machines incluses.
Visibility verification
Une fois que la définition ident_def de l'identificateur ident est trouvée, il faut vérifier que cette définition est visible. Notons : - ¿ la nature de ident_def (au sens de T_access_entity_type), - ¢ la localisation de ident_def (au sens de T_access_entity_location). - Ã le type de ident (au sens de T_access_from_context). Alors, avec les notations, si ± = (¿;¢; Ã), il faut que ± soit compatible avec l'utilisation qui en est faite. Par exemple, si ident est en partie gauche d'une affectation, il faut que ± vaille AUTH_READ_WRITE.
Requirement for software engineering
Le compilateur B doit pouvoir produire, au moyen d'une option d'appel dédiée, une sortie aux
Fourth part : Datas typing of component
Chapter 13 : Presentation
Cette partie détaille les aspects liés au typage des données du Betree. La dernière passe de l'analyse sémantique consiste à typer les noeuds de l'arbre, vérifier la validité des formules qu'il contient, et associer des types aux identificateurs du composant. Cette passe permet donc d'enrichir le Betree d'informations de type. Le Chapter 14 présente la modélisation employée dans le Betree pour représenter ces types. Le Chapter 15 présente les exigences de typage d'un composant. Ce sont ces exigences qui dirigent la passe de typage des données du composant. Elles se basent notamment sur : - Des exigences de vérification de type, détaillées au Chapter 17. - Des contraintes propres au typage des identificateurs, présentées au Chapter 16. Si la passe de typage se termine avec succès, le Betree est déclaré sémantiquement correct.
Conventions used in this part
Les notations suivantes sont utilisées dans cette partie : - On désigne par ¡(ident) le type B de ident. - On désigne par ª(X) le type B Setof(X), oµu X est un type B1. - On désigne par ½ la fonction qui à un type B de base associe le même type, dans lequel les bornes sont mises à NULL2. - On désigne par Ensemble_Index_Large un ensemble de base (ensemble prédéfini, abstrait, énuméré ou intervalle), un ensemble en extension ou un identificateur. Le type B d'un Ensemble_Index_Large est de la forme ª(K(T;U; V )), oµu T est un type de base et U et V ses bornes, qui doivent être établies. - Les bornes inférieures et supérieures d'un ensemble A seront notées A¡ et A+.
Chapter 14 : b type modelisation
Types in B
D'après [BBOOK] et [REF B], un type B est soit un type de base, soit un constructeur de type.
Basic types
Les types de base sont : - L'ensemble des entiers relatifs Z, - L'ensemble des booléens BOOL, - L'ensemble des cha^³nes de caractères STRING, - Les ensembles abstraits et les ensembles énumérés introduits dans la clause SETS ainsi que les paramètres formels ensemblistes de la machine.
Constructors
Les deux constructeurs de type sont : - L'ensemble des sous-ensembles, noté SetOf. - Le produit cartésien, noté ¤.
First modelisation
Introduction
Cette première modélisation présente la représentation historique des types au sein du \Type Checker". Par historique, nous désignons la modélisation utilisée avant les évolutions de 1996, spécifiées dans [NOTE3] et [NOTE4], et destinées à représenter les tableaux.
Comme ces évolutions se caractérisent par des ajouts dans la modélisation, et ne remettent pas en cause ses fondements, nous choisissons de présenter progressivement la modélisation employée dans le compilateur B. Dans cette section, seule cette \première" représentation est décrite. Dans la section 14.3, notre représentation sera améliorée dans le but de représenter les types tableaux.
Representation in the "Type Checker" of the first channel
- Type de base : - Ensembles prédéfinis : btype(ENS), oµu ENS vaut INTEGER, BOOL ou STRING. - Ensemble abstrait ENS : atype(ENS). - Ensemble énuméré ENS : etype(ENS). - Constructeur Setof : Setof(type). - Constructeur ¤ : type * type. Le type ttype est utilisé pour \typer" une variable locale qui n'a jamais été utilisée.
Representation within the compiler B
Introduction La représentation au sein du compilateur B reproduit, sous forme d'une hiérarchie de classes, la modélisation utilisée au sein du Type Checker pour les raisons suivantes : - La tra»cabilité est immédiate, non seulement avec le Type Checker, mais plus généralement avec [REF B] et [BBOOK]. - Nous savons, gr^ace à la cha^³ne actuelle, que cette modélisation est satisfaisante et su±- sante. Modélisation à l'aide de classes La classe T_type factorise les propriétés communes aux types du compilateur B. La figure 14.1 illustre la hiérarchie des classes qui modélisent les types au sein du compilateur B. Les classes suivantes, qui héritent de T_type, définissent les types \terminaux" : - Type de base : Les types de bases sont modélisés au moyen de la sous-classe T_base_type de T_type. Cette classe a elle-même trois sous-classes, qui sont les suivantes : - Ensembles prédéfinis : instance de T_base_type. Le champ type permet de spécifier le type prédéfini. L'ensemble énuméré T_builtin_type, décrit dans le tableau 14.2, est utilisé pour implémenter ce champ. - Ensemble abstrait ENS : instance de T_abstract_type. Le champ type_definition, de type T_ident *, permet de référencer la définition de ENS. Le champ after_valuation_type, de type T_type *, permet de conna^³tre le type après valuation d'un type abstrait 1. Exemple : - MACHINE AA SETS ENS END Le type de ENS est un T_abstract_type de name ENS. - IMPLEMENTATION AA_1 REFINES AA VALUES ENS = INT END Le type de ENS est toujours le T_abstract_type précité, mais son champ after_ valuation_type pointe sur un T_setof_type qui décrit INT. Par défaut, c'est le type après valuation qui est nécessaire à l'inférence de type. Toutefois, pour des raisons de tra»cabilité utiles notamment lors de la traduction de B vers un langage cible, il est important de pouvoir référencer le type avant valuation.
Pour cela, la classe T_type définit deux méthodes virtuelles : la méthode get_real_type, qui donne le type après valuation, et la méthode get_spec_type, qui donne le type avant valuation. Ces méthodes sont bien s^ur redéfinies dans la classe T_abstract_type, ainsi que dans les constructeurs de type afin de les propager. - Ensemble énuméré ENS : instance de T_enumerated_type. Le champ type_definition, de type T_ident *, permet de référencer la définition de ENS. - Constructeurs de type : Les constructeurs de type sont modélisés au moyen de la sous-classe T_constructor_type de T_type. Cette classe a elle-même trois sous-classes, qui sont les suivantes : - Constructeur Setof : Instance de T_setof_type. Le champ base_type, de type T_type *, permet de référencer le type dont on exprime l'ensemble des sous-ensembles. - Constructeur ¤ : Instance de T_product_type. Les champ type1 et type2, de type T_type *, permettent de modéliser les deux types dont on exprime le produit carté- sien. La modélisation de cette classe a changé depuis la version 1.1 de ce document car dans les versions précédentes, cette classe contenait une liste de types. Cette modélisation était \plus pratique" pour parcourir les listes mais ne permettait pas de différencier le type de A ¤ B ¤ C et A ¤ (B ¤ C). Cette différenciation est primordiale dans les expressions de relations, par exemple pour calculer le domaine d'une expression : dom(A ¤ B ¤ C) = A ¤ B et dom(A ¤ (B ¤ C)) = A. Avec une modélisation binaire similaire à celle employée pour les expressions, ces problèmes n'existent plus. - Constructeur de type enregistrement : Instance de T_record_type. Les types des labels sont cha^³nés dans la liste first_label_type, last_label_type et modélisés au moyen de la classe T_label_type décrite ci-après. - Type générique : la classe T_generic_type est utilisée pour modéliser un type générique. Ce type est employé pour typer les identificateurs prédéfinis -} et [], dont les types sont respectivement compatibles avec tous les ensembles, et toutes les séquences : - le type de -} est Setof(?) - le type de -} est Setof(Z * ?) Le type ? représente une instance de la classe T_generic_type. Un type générique n'a pas de sens dans l'absolu, dans un source B sémantiquement correct, les types génériques sont toujours des types génériques \de quelque chose". Ainsi, dans l'expression x <: INT & x = -}, le type générique est instancié en Setof(INT). Par contre, une expression comme -} = -} est sémantiquement incorrect. De même, une expression dont le type contient un type générique non instancié n'est pas typante. La classe T_generic_set possède un champ type de type T_type. Ce champ vaut NULL tant que le type n'est pas instancié, et pointe sur le type qui instancie sinon.
- Type champ d'enregistrement : la classe T_label_type est utilisée pour modéliser le type d'un champ d'enregistrement. Le champ name, de type T_ident * et éventuellement NULL, permet d'accéder au label du champ. Le champ type de type T_type * permet quant à lui d'accéder au type du champ. Les variables locales qui ne sont pas utilisées, et plus généralement les données non typées, sont déterminées par leur champ type qui vaut NULL, i.e. on ne modélise pas la structure ttype du Type Checker.
Final modelisation
Principle
Comme décrit dans les documents [NOTE3] et [NOTE4], pour pouvoir traduire les type tableaux, il faut ajouter à la modélisation des types B une notion de borne inférieure et de borne supérieure. Au sein du Type Checker, la notation xtype(ENS) est étendue en xtype(ENS, debut, fin), oµu debut et fin désignent respectivement les bornes supérieures et inférieures de ENS. La valeur ? est utilisée lorsque l'information concernant les bornes de l'intervalle n'est pas établie, ou est inutile. Au sein du compilateur B, la classe T_base_type est enrichie de deux champs, lower_bound et upper_bound, tous deux du type T_bound décrite ci-après. Ces deux champs servent à mo- déliser les bornes inférieures et supérieures de l'intervalle. La valeur NULL est utilisée lorsque l'information concernant les bornes de cet intervalle n'est pas établie, ou est inutile. La classe T_bound exporte les méthodes suivantes : Méthode Sémantique T_ident *get_set() Accès à l'ensemble dont l'instance est une borne int get_is_lower() TRUE si borne inférieure, FALSE sinon T_expr *get_value() Valeur le cas échéant
Particular modelisation in abstract cases
Les bornes des ensembles abstraits ne peuvent pas être déterminées dans le cas général puis- qu'elles ne sont connues qu'au moment de leur valuation, dans la clause VALUES d'une implé- mentation. Ainsi, le Type Checker représente systématiquement les bornes d'un ensemble A par la notation [A et ]A. Ces bornes ne sont jamais valuées. Dans le compilateur B, les bornes sont modélisées au moyen d'instance de la classe T_bound. Si elles sont valuées, le champ value de l'instance correspondante de la classe est mis à jour.
Types identifiers predefined
Le tableau ci-après présente les types des identificateurs prédéfinis, qui sont les bases utilisées pour le calcul de type par inférence. Les entités correspondantes, qui sont des \builtin" du compilateur, sont crées et typées lors de la phase d'initialisation du compilateur.
Immediates types
Un certain nombre de structures de données ont un type \immédiat" en B. En effet, on peut attribuer à ces données un type sans recourir au mécanisme générique d'inférence de type. Pour des raisons de performances, le compilateur B type ces données lors de la création de l'entité correspondante dans le Betree, c'est à dire dès la phase d'analyse syntaxique.
Type storage in the BeTree
Expressions typage
A chaque expression est associé un type, modélisé par une instance de T_type. Ce type est calculé par inférence au cours de la phase d'inférence de types. Dans les substitutions, les expressions ou les prédicats faisant intervenir plusieurs expressions, les types de toutes les expressions sont calculés. Le Chapter 17 détaille cette étape. La compatibilité de ces types est ensuite vérifiée. Dans le cas de types \records", pour que deux types soient compatibles, ils doivent avoir le même nombre de labels. Ces labels doivent être compatibles deux à deux : même type, et impossibilité d'avoir un champ \sans label" (i.e. un joker) simultanément dans les deux champs. Si un des champs n'a pas de label, alors on lui affecte le label du champ avec lequel on le compare.
Identifiers typage
Le type des identificateurs est sauvegardé dans leur définition. Le principe, illustré dans la figure 14.3, est le suivant Le Chapter 16 détaille cette étape. Si on affecte un \type record" à un identificateur qui n'a pas encore été typé, il faut vérifier qu'aucun des champs de ce type record n'est un joker (i.e. tous les types des champs doivent contenir un label).
Valuation of abstract sets
Lorsqu'un ensemble abstrait est valué, on dit que son type est \plongé". Toutes les données dont le type dépend de cet ensemble abstrait doivent être à nouveau typées. Par exemple, si dans une machine abstraite on a : MACHINE AA SETS ENS CONCRETE_VARIABLES var INVARIANT var : ENS
END et si dans son ra±nement on a : IMPLEMENTATION AA_1 REFINES AA VALUES ENS = 1..5 INITIALISATION var := 1 END Alors le type de var dans AA est T_abstract_type(ENS,ENS-,ENS+). Dans AA_1, comme ENS est valué, le type de var est T_predefined_type(BTYPE_INTEGER, 1, 5). Le typage fort de var dans AA_1 est nécessaire dans l'optique de la traduction de tableaux. Cependant, seul le typage de la machine abstraite permet de savoir que var est un élément de ENS, ce qui est important pour la traduction. Ainsi, dans notre exemple : - Dans la spécification, le type de var est T_abstract_type(ENS, ENS-, ENS+), avec set = ENS - Dans l'implémentation, le type de var est T_predefined_type(BTYPE_INTEGER, 1, 5), avec spec_type qui vaut T_abstract_type(ENS, ENS-, ENS+). Le paragraphe 14.2.3 page 69 décrit la modélisation employée pour garder la tra»cabilité avec le type abstrait originel tout en poursuivant l'inférence de types avec le type \plongé". INITIALISATION
Chapter 15 : typage requirement
Le typage d'un composant se déroule comme suit : - TYPE 1 : typer récursivement toutes les machines requises, après avoir vérifié que lors d'une inclusion, d'une extension ou d'une importation avec instanciation, tous les para- mètres formels sont valués, avec des paramètres effectifs dont le type est compatible avec les paramètres formels. Les données du composant utilisé doivent être re-typées car leur type peut dépendre de la valuation des paramètres formels. Comme exposé au paragraphe 14.6.3 page 73, le champ spec_type est utilisé pour modé- liser le type des données \avant valuation". - TYPE 2 : typer tous les identificateurs du composant, selon les règles présentées au Chapter 16 - TYPE 3 : typer toutes les clauses non encore typées du composant, selon les règles présen- tées au Chapter 17. Par typage, on entend non seulement effectuer des vérifications de types, mais également calculer par inférence les types des identificateurs des composants. Le Chapter 16 présente les exigences relatives au typage par inférence des identificateurs. Ces exigences sont complétées par les exigences de contrôle de types, présentées au Chapter 17.
Chapter 16 : B identifiers typage
Presentation
Comme présenté au paragraphe 14.6.2, le type des identificateurs B est sauvegardé dans leur définition. ETYPE 1:la règle suivante doit être respectée dans toute utilisation d'un identificateur :
Un identificateur doit avoir été typé avant d'être lu
et, conformément à ETYPE 2, un record en extension sans label, de la forme (X1,...,Xn) ne peut pas être utilisé pour typer une donnée. Les identificateurs sont typés dans des clauses dédiées : le paragraphe 16.4 précise, pour chaque type d'identificateur, la clause dans laquelle il doit être typé. En outre, le typage effectif des identificateurs dans ces clauses doit obéir à des règles qui s'ajoutent à celles présentées au Chapter 17. Dans la pratique, les identificateurs sont typés dans l'un des langages suivants : - Dans le langage des prédicats. Seuls les prédicats de typage permettent de typer les identificateurs. Dans les autres prédicats, on se contente de vérifier les types, sans toutefois mettre à jour le type des identificateurs. Par exemple, le prédicat x = 2 => y : INT ne type ni x, ni y. Le paragraphe 16.2 décrit les modalités du typage dans ce langage. - Dans le langage des substitutions. Le paragraphe 16.3 décrit les modalités du typage dans ce langage. Les tableaux présentés dans la suite de ce Chapter sont composés de lignes qui décrivent des cas de typage. Dans chaque ligne, les deux premières colonnes expriment des contraintes sur les données en partie gauche et en partie droite de la formule qui type. Le symbole £ dénote une absence de contrainte. Les cas se lisent dans leur ordre d'apparition, à la manière d'un IF .. THEN .. ELSE.
Typing in the language of predicate
Seuls sont décrits ici les prédicats de typage (appartenance, inclusion, égalité). Les autres pré- dicats ne sont pas des prédicats typants, et ne sont donc pas traités dans ce Chapter.
Affiliation : ITYPE 1-1
Syntaxe A : B Le type de B doit être un ensemble, et il doit y avoir autant de types en partie droite que d'identificateurs en partie gauche.
Include : ITYPE 1-2
Syntaxe A <: B ou A <<: B Typage résultant
Egality : ITYPE 1-3
Syntaxe A = B Typage résultant
Typage in substitutions case
Affiliation : ITYPE 2-1
Syntaxe A := B Typage résultant
Operation return : ITYPE 2-2
Syntaxe A < ¡ ¡ B Typage résultant Notons ff le (ou les) paramètres de sortie de l'opération B
Become an element of : ITYPE 2-3
Syntaxe A :: B Typage résultant
Decome as : ITYPE 2-4
Syntaxe A : B Typage résultant
Localisation of identifiers typage
Chaque type d'identificateur doit être typé à un endroit spécifique d'un composant B. Cette section présente, pour chaque type d'identificateur, la localisation de son typage. Les éventuelles restrictions de type applicables à chaque catégorie d'identificateurs sont égale- ment présentées.
Typage of formals parameters : LTYPE 1
Paramètre formel de type ensemble : LTYPE 1-1 Un paramètre formel dont le nom ne comporte pas de caractère minuscule est un paramètre formel de type ensemble. Il ne doit pas être typé. Les paramètres formels de type ensemble sont incompatibles. Il est donc interdit, par exemple, d'exprimer qu'un paramètre ensemble est contenu dans un autre. Paramètre formel scalaire : LTYPE 1-2 Un paramètre formel dont le nom comporte au moins un caractère minuscule doit être typé dans la clause CONSTRAINTS du composant. Il peut donc être de type scalaire ou ensembliste. Les seuls types autorisés sont : Z, BOOL ou un paramètre ensemble de la machine.
Constants typage : LTYPE 2
- LTYPE 2-1 : Chaque constante, concrète ou abstraite, définie dans un composant et qui n'est pas homonyme à une constante de l'éventuelle abstraction du composant doit être typée dans la clause PROPERTIES du composant. - LTYPE 2-2 : Chaque constante définie dans un ra±nement ou une implantation et qui est homonyme à une constante de l'abstraction ne doit pas être typée. Elle hérite du type défini dans l'abstraction Typage des constantes concrètes LTYPE 2-3 : Une constante concrète ne peut avoir que l'un des types suivants : - Entier, booléen, - élément d'ensemble abstrait ou énuméré, - Intervalle fini et non vide de Z ou d'un ensemble abstrait, - Tableau.
Typage des variables : LTYPE 3
Principe Source : - LTYPE 3-1 :Chaque variable, concrète ou abstraite, définie dans un composant et qui n'est pas homonyme à une variable de l'éventuelle abstraction du composant doit être typée dans la clause INVARIANT du composant. - LTYPE 3-2 :Chaque variable définie dans un ra±nement ou une implantation et qui est homonyme à une variable de l'abstraction ne doit pas être typée. Elle hérite du type défini dans l'abstraction Typage des variables concrètes LTYPE 3-3 : Une variable concrète ne peut être que de type scalaire ou tableau.
Typage des ensembles : LTYPE 4
LTYPE 4 : Les ensembles abstraits et énumérés sont typés de fait par leur déclaration dans la clause SETS.
Typage des paramètres d'opération : LTYPE 5
Typage dans une machine abstraite - LTYPE 5-1 :Les paramètres formels d'entrée d'une opération doivent être typés dans le corps de l'opération, au sein d'un prédicat de typage. - LTYPE 5-2 :Les paramètres formels de sortie d'une opération doivent être typés dans le corps de l'opération, dans le texte qui précède son utilisation, au moyen d'une substitution typante. Typage dans un ra±nement ou une implémentation LTYPE 5-3 : Les paramètres formels ne sont pas typés. Ils héritent du type qui leur est affecté dans la machine abstraite. LTYPE 5-4 : La liste ordonnées des paramètres formels doit rester identique au cours du ra±- nement.
Typage des variables locales : LTYPE 6
Les variables locales sont introduites dans les substitutions VAR L IN S END. Elles sont typées lors de leur première utilisation dans l'ordre des substitutions constituant S. Dans le cas d'une initialisation dans des instructions IF, WHILE, . . . , il n'est pas toujours possible de savoir si une variable locale est typée avant d'être lue. C'est le cas dans l'exemple suivant : MACHINE M OPERATIONS op = VAR y IN IF xx = 1 THEN yy := TRUE END IF yy = TRUE THEN xx := xx + 1 END END Dans ce cas, yy peut être lu avant d'être initialisé. Le Type Checker effectue un contrôle statique, et émet un message d'avertissement s'il détecte de telles situations. Le document [NOTE1] préconise quant à lui l'ajout d'une substitution de type précondition pour générer une obligation de preuve. Le comportement du compilateur B reste à préciser.
Locating the valuation identifiers
Valuation constants and ensembles : LVAL 1
Ensembles abstraits et constantes : LVAL 1-1 Les ensembles abstraits et les constantes qui ne sont pas implantés par homonymie sont valués dans la clause VALUES d'une implémentation. Ensemble énuméré : LVAL 1-2 Les ensembles énumérés ne sont pas valués
Variables initialisation : LVAL 2
Toutes les variables d'un composant doivent être initialisées dans la clause INITIALISATION, aussi bien dans une machine abstraite que dans un ra±nement et une implémentation. Cas particulier : dans un ra±nement et dans une implémentation, les variables collées par ho- monymie avec une variable provenant d'une machine requise ne sont pas initialisées.
Instanciation of the parameters of a machine imported : LVAL 3
L'instanciation d'un paramètre ensemble d'une instance de machine importée, ne peut pas être un intervalle vide.
Chapter 17 : Type verification
Definitions
Set
Les différents types d'ensembles possibles sont les suivants : - Un ensemble de base : - Ensemble d'entiers : ª(btype(INTEGER)) - Ensemble de booléens : ª(btype(BOOL)) - Un ensemble abstrait : ª(atype(ENS)) - Un ensemble énuméré : ª(etype(ENS)) - Un ensemble en extension : ENS = x1; : : : xn, dont le type est ª(¡(x1) ¤ : : : ¡(xn)) - Un produit cartésien de n ensembles ENS = E1 ¤ : : :En, dont le type est ª(¡(E1) ¤
- : : ¡(En))
The 3 control types
Les tableaux présentés dans ce Chapter présentent les exigences de typage pour chaque type de constituant d'un composant B. Ces contrôles de base peuvent, le cas échéant, être enrichis de vérifications supplémentaires : - Mise à jour des bornes non établies dans l'expression de gauche à partir des bornes cor- respondantes dans l'expression de droite. On parle alors de contrôle avec mise à jour - Vérification de l'égalité des bornes de l'expression de gauche avec celles de l'expression de droite. En particulier, les bornes de l'expression de gauche doivent déjà avoir été position- nées. On parle alors de contrôle fort
/*
* * LOTS OF BLACK HOLE WITH BOARD, EDIT MAYBE LATER BUT BECOME THERE ARE TOO MUCH BOARD, WE DON'T *CONTINUE * */