Traducteurs de l`Atelier B
Contents
1. Un module qui initalise une pile d une taille donn e et qui permet d empiler ou de d piler un l ment Un module qui affiche une pile L exemple devra cr er deux piles de taille diff rentes et prouver par affichage de leur contenu que les piles sont bien initialis es et que les proc dures d empilement et de d pilement fonctionnent Remarque importante Cet exemple et les codes sources B pr sent s ci dessous pour sa r alisation n a aucune pr tention au niveau du langage B Il ne se veut pas un exemple de style de conception B mais tout simplement un exemple complet de cr ation de projet avec traduction en langage cible puis ex cution du code produit Ainsi pour g rer des piles non born es nous aurions pu les implanter sur la machine de base BASIC_ARRAY_VAR la place d un tableau statique born LES EXEMPLES NE SONT PAS ADAPT S UNE TRADUCTION HIA CAR LES TYPES TABLEAUX NE SONT PAS D CLAR S EXPLICITEMENT voir Vanneze B pour plus de d tails APRES CHAQUE EXEMPLE NOUS EXPLICITERONS LES MODIFICATIONS R ALISER POUR R ALISER UNE TRADUCTION AU MOYEN DU TRADUCTEUR HIA 19 20 Traducteurs de l Atelier B Manuel Utilisateur 4 1 3 Architecture du projet et code B Le composant pile Le composant pile mod lise une pile d entiers naturels La taille de la pile est param trable c est un param tre de la machine sous r serve de ne pas d passer 10 l ments car pour simplifier notre exe2. objets des bibliotheques S mantique Valeur par d faut Valeur par d faut Traducteurs Ada HIA Traducteurs C C Change le nom du compilateur cible A gnatgcc T gcc Change le suffixe des fichiers objets B bod B bdy de type corps de paquetage Affiche les conflits de noms et leur r solution c c Informations de compilation sur le logiciel C I Affiche la configuration avant de faire l dition D D Change le nom de l diteur de liens cible K gnatbl K gcc Change la taille maximale en caract res des 1 80 1 80 lignes produites Ajoute un chemin de recherche pour les fichiers L L Change la valeur de MAXINT M 2147483647 M 2147483647 Change la valeur de MININT N 2147483647 m 2147483647 Demande une dition de liens pour projet h t rog ne n n Change le suffixe des fichiers objets O blf O blf de type B Link File Change le r pertoire o les fichiers sont g n r s P lang P lang Change le suffixe des fichiers objets S str S spe de type sp cifications de paquetage Change la valeur en caract res d une tabulation t 4 t 4 G n re du code Ada dont lex cution produit des traces sur les op rations appel es et les non dispo valeurs des param tres Mode verbeux v v Num ro de version et usage du logiciel V V FIG 5 3 Options utilisables lors de l dition des liens d un projet 34 Traducteurs de l Atelier
3. Exemple de fichier B Link File Annexe B Sp cificit s du language BO accept par le traducteur HIA B 1 Introduction Le traducteur HIA utilise un langage BO qui lui est propre Ces sp cificit s sont caus es D une part par le typage explicite par identificateur des tableaux et des articles D autre part par la volont de g n rer un code simple et en particulier des paquetages Ada proches des composants B regroupant notamment les d clarations des constantes et des param tres formels Nous d signerons par BO HIA ce langage dans la suite de ce chapitre B 2 Traduction des tableaux B 2 1 Principe Pour pouvoir tre traduite par le traducteur HIA une donn e de type tableau doit imp rativement avoir t typ e explicitement par un identificateur c est dire par ap partenance une donn e qui d finit un type tableau c est une restriction par rapport au langage BO classique Les donn es qui d finissent les types tableaux sont des constantes concr tes qui doivent tre typ es par galit avec un type tableau B C est ce type B d finit dans la clause PROPERTIES qui est utilis pour la traduction la valuation est ignor e Nous pr conisons de recopier le typage de la clause PROPERTIES dans la clause VALUES pour viter toute confusion La possibilit de d finir une constante concr te de type tableau est une extension par rapport au langage BO classique B 2 2 Exemple
4. param tre formel El ment de paquetage T set de type ensemble g n rique ADA O Sous type HIA tableau array T_array_x x dim du tableau Fig A 2 Traduction des types BO en Ada HIA C et C A 4 1 M thode d crire du code cible en Ada CETTE SECTION NE S APPLIQUE QU AU TRADUCTEUR ADA Le nom du paquetage est le m me que le nom de la sp cification B en utilisant in diff remment des majuscules ou des minuscules Par contre les noms de fichiers utilis s doivent tre en minuscules Soit P ce nom Le paquetage P doit d finir Le type TYPE_P qui est un record qui doit comporter obligatoirement un champ initialisation de type BOOLEAN Dans ce record on place toutes les structures de donn es n cessaires la mod lisation des instances de chaque machine Le type PTR_P de type pointeur sur P Une proc dure IMPORTS qui prend en entr e un param tre this de type PTR_P et qui d crit l instance importer puis autant de param tres en entr e que de param tres formels de type scalaire La figure A 2 donne la correspondance entre les types BO et les types en langage cible Une proc dure INITIALISATION qui prend en entr e un param tre this de type PTR_P et qui d crit l instance importer Autant de proc dures que d op rations de la machine Les proc dures ont le m me nom que dans la sp cification B pr c d du nom de la machine en minu
5. Dans le cas d un projet autonome le service d dition des liens prend en entr e le nom de la sp cification d une impl mentation destin e tre le point d entr e d un projet ainsi que le nom d un module de lancement cr er et cr e L ensemble des fichiers sources interfaces et corps des composants du projet DANS LE CAS DU TRADUCTEUR HIA LES FICHIERS SONT DUPLIQU S POUR CHAQUE INSTANCE DE COMPOSANT Le code cible du module du lancement du projet L interface et le corps du module sets en ADA et HIA ou SETS en C C pour les types tableaux inf r s les constantes concr tes les ensembles abstraits et les pr d finis succ pred MAXINT MININT PR SENTATION DU LOGICIEL 9 O POUR LE TRADUCTEUR HIA CE FICHIER NE CONTIENT QUE LES ENSEMBLES ET FONCTIONS PR D FINIS Le fichier makefile permettant de g n rer le projet Pour tre utilisable comme point d entr e d un projet une impl mentation doit poss der une et une seule op ration qui ne poss de aucun param tre tant en entr e qu en sortie Par contre le nom de cette op ration est libre L diteur de liens parcourt r cursivement les liens d importation de cette machine et tra duit ainsi en code cible terminal l ensemble des fichiers objets utilis s par le projetP Les fichiers objets sont recherch s dans le r pertoire lang du projet en cours de traduc tion puis dans les r pertoires lang des bibliot
6. affiche Resultat attendu PILE VIDE Resultat effectif la pile est vide Affichage de la pile vide Resultat attendu PILE VIDE Resultat effectif la pile est vide On remplit la pile puis on l affiche Resultat attendu PILE PLEINE Resultat effectif fond de la pile 1 2 3 4 haut de la pile On vide la pile puis on l affiche Resultat attendu PILE VIDE Resultat effectif la pile est vide FIN DU TEST FIG 4 7 Ex cution du programme PILE 28 Traducteurs de l Atelier B Manuel Utilisateur Instance Chemin d acc s en Ada Chemin d acc s en C C demo this entry BASIC IO this ref BASIC IO entry gt ref BASIC IO interface A interface pile this ref interface A entry ref interface A interface B interface pile this ref interface B entry ref interface B pile cr e par entry ref interface A interface A interface pile this ref interface A ref pile ref pile pile cr e par entry gt ref interface B interface B interface pile this ref interface B ref pile ref pile affiche pile cr e par entry ref interface A interface A interface pile this ref interface A ref pile ref affiche pile affiche pile cr e par entry ref interface B interface B interface pile this ref interface B ref pile ref affiche pile FIG 4 8 Correspondance entre les instances physiques du projet et leur chemin d acc
7. ne peut se faire qu au cours d une phase d dition des liens pendant laquelle le Traducteur a une vue globale de l ensemble d un projet Cr ation des instances de composants CETTE SECTION NE S APPLIQUE QU AU TRADUCTEUR HIA L diteur est lien est responsable de la duplication copie physique des fichiers des fichiers pour chaque instance des composants du projet Ainsi si on utilise dans un projet deux instances M1 et i1 M1 d un composant M1 alors l diteur de liens cr e deux paquetages Le paquetage M1 dans m1 ads et m1 adb Le paquetage i1 M1 dans i1_m1 ads et i1_m1 adb Ce paquetage est obtenu par copie du paquetage M1 et remplacement de toutes les occurences de M1 par il M1 Valuation des parametres formels CETTE SECTION NE S APPLIQUE QU AU TRADUCTEUR HIA Le traducteur HIA d clare les param tres formels dans les paquetages associ s Il doit donc d finir dans chaque paquetage qui a des param tres formels non seulement le nom et le type de ces param tres mais aussi leur valeur Or la valeur effective d un param tre formel n est connue que lors de l importation du module par un autre module du projet exemple dans M1 la clause IMPORTS M2 10 c est dans M1 que l on conna t la valeur 10 du param tre formel param de M2 Mais c est dans M2 qu il faut crire param constant INTEGER 10 L diteur de liens doit donc mettre en place les valeurs effectives des param tres formel
8. o OPTIONS est une combinaison des options pr sent es dans le tableau 5 3 et trad est donn par le tableau Remarque Une option permet de changer le nom du compilateur cible lors de l dition des liens Le fichier makefile produit instancie la variable ADA_COMPILE ou CPP_COMPILE avec cette valeur On peut toujours changer cette valeur apr s coup soit en la modifiant directement dans le makefile soit en la passant dans la ligne de commande comme dans l exemple ci dessous make ADA_COMPILE mon_compilateur_ada make CPP_COMPILE mon_compilateur_c 5 3 Traduction d un projet en Ada avec traces CETTE SECTION NE CONCERNE QUE LE TRADUCTEUR ADA 31 32 Traducteurs de l Atelier B Manuel Utilisateur Option S mantique Valeur par d faut Valeur par d faut Traducteurs Ada HIA Traducteur C C B Change le suffixe des fichiers objets bod bdy de type corps de paquetage D Affiche la configuration avant de traduire C Informations de compilation sur le logiciel I Ajout un chemin d acc s pour la recherche des sources B l Change la taille maximale en caract res des 80 80 lignes produites O Change le suffixe des fichiers objets blf blf de type B Link File P Change le r pertoire de sortie lang lang S Change le suffixe des fichiers objets str spe de type sp cification ou interface t Change la valeur en caract res d une tabulation 4 4 T Ada G
9. sireux de trouver plus d informations sur leur utilisation pourra s y reporter Les machines de base sont les seuls moyens offerts Putilisateur d implanter certaines des fonctionnalit s des sp cifications Ainsi la seule facon d implanter un tableau dynami que Pest l importation de BASIC ARRAY VAR une dimension ou BASIC ARRAY RGE deux dimensions tie un tableau dont la taille d pend des param tres de la machine 37 38 Traducteurs de l Atelier B Manuel Utilisateur MACHINE DESCRIPTION BASIC ARRAY RGE Implantation d un tableau a deux dimensions BASIC ARRAY VAR Implantation d un tableau a une dimension BASIC IO Entr es Sorties de base FIG A 1 Machines de base livr es avec 1 Atelier B A 3 M thode d criture d une machine de base Une machine de base crite par l utilisateur est compos e de quatre l ments 1 Une sp cification en B 2 Une interface ou sp cification crite en langage cible 3 Un corps de paquetage ou de classe crit en langage cible 4 Un fichier au format B Link File destin l diteur de liens La m thode la plus simple pour crire une machine de base est 1 Ecrire la sp cification en B 2 Ecrire une impl mentation coquille vide c est dire o toutes le corps des op rations contient skip 3 Faire traduire l impl mentation par l atelier B 4 Garder le fichier B link file et remplir les sq
10. tr par la taille de la pile cr er Il cr e une pile de cette taille l affiche pour v rifier qu elle est vide la remplit avec des entiers cons cutifs puis l affiche pour v rifier qu elle est pleine La pile est alors vid e de ses lements puis affich e pour v rifier qu elle est vide La pile est cr e par importation du composant pile Elle est remplie puis vid e au moyen des op rations empiler et depiler de ce composant L importation du composant affiche_pile permet d afficher la pile La figure donne le code source B de la sp cification et de l impl mentation de ce composant POUR TRADUIRE EN HIA IL FAUT TYPER LES PILES AVEC LE TYPE type tableau DE affiche pile SC NARIOS D EXPLOITATION 21 MACHINE pile nb elements CONSTRAINTS nb elements NAT amp nb elements gt 1 amp nb elements lt 10 CONCRETE VARIABLES la pile haut de pile INVARIANT la pile 1 10 gt NAT amp haut de pile NAT amp haut de pile gt O amp haut de pile lt nb elements INITIALISATION lapile 1 10 gt NAT haut de pile 0 OPERATIONS empiler val PRE haut de pile lt nb elements amp val NAT THEN la pile haut de pile val haut de pile haut de pile 1 END depiler PRE haut de pile gt 1 THEN haut de pile haut de pile 1 END END IMPLEMENTATION pile 1 nb elements REFINES pile INITIALISATION la pile haut de pile
11. 1 OPERATIONS demonstration skip END IMPLEMENTATION interface pile 1 nb elements REFINES interface pile IMPORTS pile nb elements affiche pile nb elements SEES BASIC IO OPERATIONS demonstration BEGIN On affiche la pile vide STRING WRITE Affichage de la pile vide affiche PILE VIDE la pile haut de pile On remplit la pile STRING WRITE On remplit la pile puis on l affiche n VAR ii IN ii 1 WHILE ii lt nb elements DO empiler ii ii ii 1 INVARIANT ii NAT ii gt 1 amp ii lt nb elements 1 VARIANT nb elements 1 ii END END On affiche la pile pleine affiche PILE PLEINE la pile haut de pile On vide la pile STRING WRITE On vide la pile puis on l affiche n VAR ii IN ii 1 WHILE ii lt nb elements DO depiler ii ii 1 INVARIANT ii NAT amp ii gt 1 amp ii lt nb elements 1 VARIANT nb_elements 1 ii END END On affiche la pile vide affiche PILE VIDE la pile haut de pile END END FIG 4 3 Sp cification et impl mentation du composant interface_pile 24 Traducteurs de l Atelier B Manuel Utilisateur IMPLEMENTATION demo 1 REFINES demo IMPORTS BASIC IO interface A interface pile 3 interface B interface pile 4 OPERATIONS demo piles MACHINE BEGIN demo STRING WRITE DEBUT DU TEST n n OPERATIONS
12. ANSI C ANSIC ou ANSI C IANSI C 2 Traducteurs de l Atelier B Manuel Utilisateur 1 3 Vue d ensemble du manuel Le chapitre 2 pr sente les objectifs du Traducteur Les environnements support s et la philosophie g n rale de traduction y sont expos s Le chapitre 3 d taille les principes d exploitation du Traducteur L utilisation au sein de l Atelier B est d crite tout comme l utilisation en ligne depuis un shell Le chapitre se termine sur l vocation des pr cautions d emploi respecter lors de l utilisation du Traducteur Le chapitre Al illustre au moyen d un exemple simple le cycle complet de d veloppement d un projet B traduit en langage cible Le cas d un projet B dont la traduction en langage cible est int gr e dans un projet plus vaste crit nativement en langage cible est voqu Le chapitre 5 r sume les options d utilisation du logiciel Il d taille ensuite le mode d uti lisation du Traducteur qui permet de g rer les configurations des projets au moyen de Poutil SCCS Enfin le chapitre 6 explicite les termes techniques utilis s dans ce document L annexe A donne la marche suivre pour d velopper des machines de base 1 4 Comment utiliser ce manuel L utilisateur d butant du Traducteur peut dans une premi re lecture se contenter d tudier les chapitres 3 et La mise en oeuvre des exemples pr sent s dans ce dernier chapitre constitue une illustration compl te d
13. B Manuel Utilisateur 5 4 Restriction d usage des traducteurs Avertissement Les traducteurs ADA C et C fournis dans la version 3 6 de l Ate lier B sont exp rimentaux Leur but est de montrer qu il est possible de traduire des impl mentations BO en langages de programmation classiques Leur utilisation n est donc pas garantie Le but de cette section est de d finir l ensemble des anomalies connues sur les traducteurs Nom de paquetage Les traducteurs ADA acceptent de g n rer des paquetages ayant le m me nom que des paquetages pr d finis du langage Le compilateur Ada d tecte donc un conflit et donc ces paquetages ne peuvent donc pas tre compil s Pour contourner cette anomalie il suffit de donner aux composants B un nom diff rent de ceux des paquetages pr d finis ADA Traduction des tableaux La traduction en ADA des tableaux l aide des composants r utilisables les machines de la famille L_ ARRAY peut tre incorrecte Le traducteur ADA peut allouer un espace tr s grand pour le tableau integer et donc saturer la m moire Comparaison de champs de records de type num r Lorsqu on compare ou 2 num r s ou tableaux ou records qui sont eux memes des champs de record provenant d une machine ext rieure les traducteurs traduisent rec champ enum au lieu de mch rec champ enum Param tres formels ensembles La traduction des param tres formels e
14. OPERATIONS empiler val BEGIN haut de pile 1 10 x 0 0 haut de pile 1 la pile haut de pile val END depiler BEGIN haut de pile END END haut de pile 1 FIG 4 1 Sp cification et impl mentation du composant pile 22 Traducteurs de l Atelier B Manuel Utilisateur IMPLEMENTATION affiche pile 1 nb elements REFINES affiche pile SEES BASIC IO OPERATIONS affiche message pile taille de pile MACHINE PEGIN affiche pile nb_elements STRING WRITE Resultat attendu STRING WRITE message CONSTRAINTS STRING WRITE nResultat effectif n IF taille de pile 0 nb_elements NAT amp THEN nb elemente 22 STRING WRITE la pile est vide n OPERATIONS a affiche fa ii message IN pile STRING WRITE fond de la pile taille de pile ae qo PRE ag message STRING amp re ii lt taille de pile pile 1 10 gt NAT Y INT WRITE pile 11 taille de pile NAT amp 3 STRING WRITE taille de pile lt nb elements dd RY mas INVARIANT END ii NAT amp END ii gt 1 amp ii lt nb elements 1 VARIANT nb_elements 1 ii END STRING WRITE haut de la pile n END END END END FIG 4 2 Sp cification et impl mentation du composant affiche_pile SC NARIOS D EXPLOITATION 23 MACHINE interface pile nb elements CONSTRAINTS nb elements NAT amp nb elements gt
15. Pour crire en BO HIA la d claration d une variable var de type tableau d entiers dont les index sont entre 4 et 12 on crira CONCRETE_CONSTANTS 43 44 Traducteurs de l Atelier B Manuel Utilisateur type_tableau PROPERTIES type_tableau 4 12 gt INT extension BO HIA VALUES type_tableau 4 12 gt INT inutilis par le traducteur CONCRETE_VARIABLES var INVARIANT var type_tableau typage explicite par identificateur impos par BO HIA INITIALISATION var 4 12 1 B 3 Traduction des articles B 3 1 Principe Pour pouvoir tre traduite par le traducteur HIA une donn e de type article doit imp rativement avoir t typ e explicitement par un identificateur c est dire par appartenance une donn e qui d finit un type article c est une restriction par rapport au langage BO clas sique Les donn es qui d finissent les types articles sont des constantes concr tes qui doivent tre typ es par galit avec un type article B C est ce type B d finit dans la clause PROPERTIES qui est utilis pour la traduction la valuation est ignor e Nous pr conisons de recopier le typage de la clause PROPERTIES dans la clause VALUES pour viter toute confusion La possibilit de d finir une constante concr te de type tableau est une extension par rapport au langage BO classique B 3 2 Exemple Pour crire en BO HIA la d claration d une vari
16. STRING WRITE illa iD n demo piles STRING_WRITE skip Demonstration avec une pile de taille maximum 3 n STRING WRITE END n interface A demonstration STRING WRITE STRING WRITE Demonstration avec une pile de taille maximum 4 n STRING WRITE interface B demonstration STRING WRITE FIN DU TEST n n END END FIG 4 4 Sp cification et impl mentation du composant demo Le composant demo Le composant demo est charg e de lancer l ex cution de application Il ne poss de qu une seule op ration qui cr ee puis teste les deux piles Ce composant sera le point d entr e du projet B C est lui qui est la racine de Varbre d importation du projet comme le montre la figure La figure donne le code source B de la sp cification et de l impl mentation de ce composant Entre autres c est lui qui importe la machine de base BASIC Id car plusieurs composants du projet vont produire des affichages l cran y compris le composant demo et nous savons qu il faut respecter la r gle un anc tre dans le graphe d importation ne peut pas faire de SEES Machine qui permet de r aliser des entr es sorties d crite dans Vannexe A SC NARIOS D EXPLOITATION 25 L gende interface interface B Lien IMPORTS gt Lien SEES 4 interface_pile interface pile 1 BASIC IO affiche pile pile LIBRARY af
17. The SPARK approach John BARNES Addisson Wesley ISBN 0 201 17517 7 Manuel de r f rence de l Atelier B Composants r utilisables Manuel de r f rence 47 Index dition des liens 9 autonome BO impl mentation v rificateur Batch mode de 1 Atelier B biblioth que 6 classe C corps sp cifications compilation 5 6 fichier makefile du projet 9 composant O corps sp cifications conflits d identificateurs 6 environnement HP UX Linux Solaris Sun Os fichiers objets 6 h t rog ne HP UX IHM de Atelier B impl mentation BO instance implicite Linux machine de base p crite par l utilisateur code offensif livr e avec l Atelier B makefile o Mode Batch de 1 Atelier B module d acc s module de d marrage module de lancement paquetage Ada corps sp cifications paquetage d acc s point d entr e 9 preuve projet module d acc s module de d marrage module de lancement paquetage d acc s point d entr e 9 Restrictions sur les noms de modules et de projets sets 9 Solaris Sun Os traduction article avec traces collage implicite compatibilit crois e et preuve MAXINT MININT point d entr e 9 portabilit renommage 7 tableau taille des lignes v rificateur aux limites v rificateur de BO
18. car les fichiers objets de la biblioth que sont inexistants 2 3 4 Machines de base Le Traducteur est livr avec les sp cifications B et les fichiers objets d un ensemble de ma chines de base permettant de r aliser facilement des entr es sorties format es des tableaux index s par des ensembles num r s ou des intervalles Ces machines sont d crites dans l annexe A Par contre les fichiers objets correspondant des machines non utilis es dans le projet ne sont pas traduits 10 Traducteurs de l Atelier B Manuel Utilisateur Chapitre 3 Principes d exploitation 3 1 Les modes de fonctionnement Le Traducteur peut fonctionner dans les trois modes suivants Dans le cadre d une session de travail avec 1 IHM de l Atelier B Dans le cadre du mode batch de l Atelier B En ligne 3 1 1 Utilisation du Traducteur au moyen de PIHM Traduction d une impl mentation BO Pour traduire une impl mentation implementation imp d un projet proj au moyen de PIHM de Atelier B il faut effectuer les op rations suivanted S lectionner au moyen de la souris l impl mentation implementation imp Appuyer sur le bouton Translator Dans la fen tre qui appara t s lectionner le langage cible avec Language et choisir Selected Only pour Components Puis appuyer sur le bouton OK La traduction est alors lanc e Remarque comme nous l avons vu au paragraphe 2 1 un composant do
19. cl Ada l diteur de liens ne peut pas r soudre le conflit et la traduction en Ada choue Les restrictions qui s appliquent aux noms de modules et de projet sont les suivantes Dans un projet aucun module ne peut avoir le m me nom que le projet Le nom d un projet ne doit pas tre en conflit avec le langage cible On rappelle que le langage Ada ne diff rencie pas les majuscules des minuscules donc les r gles voqu es ci dessus sont appliquer sans tenir compte de l utilisation ventuelles de majuscules Ainsi un projet PROJET ne peut pas contenir de module projet et un projet ne peut pas s appeler ENTRY SIci on entend par nom le nom du fichier sans son extension 18 Traducteurs de l Atelier B Manuel Utilisateur Chapitre 4 Sc narios d exploitation 4 1 D veloppement d un projet B natif 4 1 1 Principe Nous allons dans cette section d velopper un exemple de projet B natif afin d illustrer les aspects suivants du d veloppement d un tel projet Influence de la traduction sur l architecture du code B crit Traduction unitaire des modules B du projet Edition des liens du projet Compilation et ex cution du code g n r Nous donnerons le mode d emploi d taill du Traducteur au moyen de photos d crans de PIHM de l Atelier B 4 1 2 Sp cifications informelles de l exemple On veut tester la gestion d une pile d entiers Pour cela on crit plusieurs modules
20. et taper make Ce r pertoire contient l ensemble des fichiers n cessaires la compilation y compris les fichiers provenant de la traduction des biblioth ques Le fichier makefile d finit galement le but clean qui permet de supprimer tous les fichiers binaires produits par le compilateur Pour utilise ce but taper make clean PRINCIPES D EXPLOITATION 15 3 2 Les entr es et sorties 3 2 1 Messages g n r es par le Traducteur 3 2 2 Cas d une utilisation en ligne ou en mode batch Le Traducteur produit des messages d crivant son fonctionnement dans la sortie standard i e stdout Il produit ventuellement des messages d avertissement sur cette m me sortie standard et des messages d erreur sur la sortie d erreur i e stderr Ainsi un script qui lance un sc nario de traduction complete peut r cup rer les r sultats dans stdout et les erreurs dans stderr comme dans l exemple suivant Fl bin sh Script qui traduit toutes les impl mentations du r pertoire courant rm f tmp res rm f tmp err for f in imp do echo Traduction de tbhia i f gt gt tmp res 2 gt gt tmp err done echo R sultat de la traduction cat tmp err less echo Erreurs survenues lors de la traduction cat tmp err less 3 2 3 Cas d une utilisation au sein de l IHM de l Atelier B Les messages sont int gr s VIHM de l Atelier B 3 2 4 Les fichiers Le Traducteur lit e
21. le langage cible et A11 L diteur de liens cr e un module charg de lancer le projet c est le module de d marrage 26 Traducteurs de l Atelier B Manuel Utilisateur home ATELIER B pile lang 1s DEMO PILES adb basic io ads interface pile blf pile bod DEMO PILES bod demo adb interface_pile bod pile str affiche pile adb demo ads interface pile str sets adb affiche pile ads demo blf makefile sets ads affiche pile blf demo bod makefile blf sets bod affiche pile bod demo str pile adb sets str affiche pile str interface pile adb pile ads basic_io adb interface pile ads pile blf home ATELIER B pile lang make gnatgcc I home ATELIER B LIBRARY lang c DEMO PILES adb gnatgcc I home ATELIER B LIBRARY lang c sets adb gnatgcc I home ATELIER B LIBRARY lang c demo adb gnatgcc I home ATELIER B LIBRARY lang c basic_io adb gnatgcc I home ATELIER B LIBRARY lang c interface pile adb gnatgcc I home ATELIER B LIBRARY lang c pile adb gnatgcc I home ATELIER B LIBRARY lang c affiche pile adb gnatbl DEMO PILES ali o DEMO PILES home ATELIER B pile lang ls 1 DEMO PILES rwxr xr x 1 ATELIER bin 205899 May 17 11 35 DEMO PILESx FIG 4 6 Compilation d un code Ada g n r par le Traducteur Ada Lors d une utilisateur au sein de l IHM de l Atelier B ce module a le m me nom que le projet 4 1 7 Compilation du code cible et ex cution de application On ouvre une session sur la machine cible Dans notre ex
22. 1 utilise un composant Mch2 param2 et que la valuation de param fait intervenir des donn es de Mch1 par exemple une constante cst1 de mchi param2 Mchi csti La valeur de Mch2 param2 fait donc intervenir Mch1 cst1 Or Mch1 cst1 n est pas visible depuis le paquetage Mch2 et ne peut pas l tre comme Mch1 utilise Mch2 alors le paque tage Mch1 fait un with de Mch2 Mch2 ne peut donc pas faire de with de Mch1 sous peine de d pendance cyclique Il n est donc pas possible de compiler le code obtenu Plus g n ralement on voit qu il n est pas possible d utiliser des donn es non litt rales pour la valuation des param tres formels de machine Cons quence Les param tres formels effectifs de machines autoris s en BO HIA sont les litt raux entiers ou bool ens 46 Traducteurs de l Atelier B Manuel Utilisateur Bibliographie ANSI C ANSLC ADA 83 ADA 95 ADA2 ADA3 SPARK ATB1 ATB2 Le langage C troisi me dition Bjarne STROUSTRUP Campus Press ISBN 2 7740 0609 2 Le langage C norme ANSI B W KERNIGHAN et D M RITCHIE Manuel de r f rence du langage de programmation Ada Alsys F vrier 1987 Ada 95 Deuxieme dition John BARNES Addisson Wesley ISBN 0 201 34293 6 Ada An Introduction Ada reference manual Henry Ledgard Springer Verlag ISBN 0 387 90568 5 et 3 540 90568 5 Ada programming manual Integrated computer systems NEW 8 80 High integrity Ada
23. 3 D veloppement d un projet h t rogene B HIA 9 CETTE SECTION NE S APPLIQUE Q AU TRADUCTEUR HIA LE D VELOPPEMENT DES PROJETS H T ROGENES POUR LES AUTRES TRADUCTEURS EST D CRIT AU Le code g n r par le traducteur HIA est tr s simple et tres proche du BO Un paquetage est cr e pour chaque instance de composant Chaque paquetage a le m me nom que le composant associ ventuellement pr fix par le pr fixe de renommage du composant suivi par un caract re _ 2Au sens IMPORTS SEES ou EXTENDS SC NARIOS D EXPLOITATION 29 Les constantes les param tres formels et les variables du composants sont traduites dans le paquetage Les op rations ont le m me nom et la m me signature qu en B Ansi le d veloppement d un projet h t rog ne B HIA n impose aucun travail suppl mentaire par rapport un d veloppement Ada HIA natif 30 Traducteurs de l Atelier B Manuel Utilisateur Chapitre 5 Liste complete des services 5 1 Traduction unitaire d une impl mentation trad OPTIONS i nom implementation suffixe o OPTIONS est une combinaison des options pr sent es dans le tableau 5 2 et trad est donn par le tableau Traducteur Logiciel Ada tbada HIA tbhia C tbcpp C tbcpp c FIG 5 1 Traduction d une implementation depuis la ligne de commande 5 2 Edition des liens d un projet trad OPTIONS o nom_executable e spec_point_entree E chemin_bed
24. 4L exemple donn est produit en mode verbeux Par d faut on obtient une sortie plus concise PRINCIPES D EXPLOITATION 13 On peut alors forcer la traduction du composant en d sactivant la fonction de d pendance commande ddm ou disable_dependence_mode et en relancant la traduction La com mande inverse pour r activer la fonction de d pendance est edm ou enable_dependence_mode dition des liens globale au projet Pour r aliser une dition des liens globale un projet on d termine le point d entr e du projet dans notre cas c est entree_1 imp et on tape la commande Langage cible Commande Ada ada_all entree_1 HIA hia_all entree_1 C ccompile entree_1 C c all entree_1 Le Traducteur P produit alors une sortie du type suivant Entering project mode Calling B linker Entering project mode Analysing module entree entree exports constantes Analysing machine constantes Creating makefile Creating ada source code for executable module projet bod Analysing instance this This instance does not have a SEES clause Analysing instance this ref_constantes This instance does not have a SEES clause Analysing imported variables of instance this This module does not import any variable Analysing imported variables of instance this ref_constantes This module does not import any variable Creating template for package sets Installing project Creating temporary bed file tmp blka04747 Exe
25. Atelier B Traducteurs de l Atelier B Manuel Utilisateur version 4 6 ATELIER B Traducteurs de l Atelier B Manuel Utilisateur version 4 6 Document tabli par CLEARSY Ce document est la propri t de CLEARSY et ne doit pas tre copi reproduit dupliqu totalement ou partiellement sans autorisation crite Tous les noms des produits cit s sont des marques d pos es par leurs auteurs respectifs CLEARSY Maintenance ATELIER B Parc de la Duranne 320 avenue Archimede Les Pl iades 111 B t A 13857 Aix en Provence Cedex 3 France T l 33 0 4 42 37 12 70 Fax 33 0 4 42 37 12 71 mail contact atelierb eu Table des matieres 1 Description du manuel 1 LL Objectif 4 a wa dun a RE a a E 1 a EE PE O A AA ne E 1 1 3 Vue d ensemble du manuel 2 1 4 Comment utiliser ce manuel 2 1 5 Conventions et syntaxe 2 1 6 Documents associ s 3 2 Pr sentation du logiciel 5 Go Ent e dc go DE a o RE NU ce te ld dd dis due q 5 RE a A Ao a 5 2 3 Services offerts 6 2 3 1 Pr ambule Motivation de la traduction en deux passes 6 2 3 2 Service de traduction automatique d une impl mentation BO en lan gag Cible 4 4 us ri aspas pe pa 8 2 3 3 Service d dition des liens 8 a de ee a ras 9 11 3 1 Les m
26. a RR o ai e A E a 43 A A 43 os oa aa 43 cda a SOR ai Tc e as e 44 AA 44 rn daa 44 B 4 Param tres formels 444 45 Table des figures 2 1 Fichiers produits pour l interface de mach 8 2 2 Fichiers produits pour le corps demachl 8 3 1 Traduction d une implementation en mode batch 12 E Dia 14 ao e 21 Es 22 ie 23 a aia a 24 a O a O A a e 25 lancen 26 ES e E E 27 4 8 Correspondance entre les instances physiques du projet et leur chemin d acces en C C ou Adal 28 5 1 Traduction d une implementation depuis la ligne de commande 31 5 2 Options utilisables lors de la traduction unitaire d un composant 32 5 3 Options utilisables lors de l dition des liens d un projet 33 A 1 Machines de base livr es avec Atelier Bl 38 A 2 Traduction des types BO en Ada HIA Cet C H1 39 A 3 Exemple de fichier B Link File 42 Chapitre 1 Description du manuel 1 1 Objectif Ce manuel utilisateur s applique aux logiciels suivants Traducteur Ada partir de la version 4 4 Traducteur HIA partir de la version 4 6 Traducteur C C partir de la version 4 4 Par la suite lorsque nous ferons r f rence au logiciel Traducteur cela signifiera que Pon voque indiff remment le traducteur Ada HIA C ou C Lorsque l on
27. a confi guration de fichiers sources et par extension des fichiers binaires r sultant de la compilation de ces fichiers sources Shell Programme d interface entre l utilisateur et le syst me d exploitation Sous Unix les principaux shells sont sh ksh bash et csh 39 36 Traducteurs de l Atelier B Manuel Utilisateur Annexe A Les machines de base A 1 Principe A 1 1 D finition Une machine de base est une machine qui poss de une sp cification en B et qui est directement implant e dans le langage cible A 1 2 Utilit Les machines de base sont utilis es pour implanter des fonctionnalit s qui ne peuvent pas tre r alis es en BO Le plus souvent ces fonctionnalit s sont des fonctionnalit s proche du syst me entr es sorties gestion dynamique de m moire L Atelier B est livr en standard avec une collection de machines de base qui permettent de r aliser des projets B qui interagissent avec un op rateur et qui utilisent des structures de donn es complexe Le paragraphe 2 d crit ces machines Pour autant un utilisateur de l Atelier peut avoir besoin d impl menter ses propres machines de base Le paragraphe A 3 donne la marche suivre pour r aliser cette t che A 2 Description des machines de base livr es avec l Atelier B Le tableau donne la liste des machines de base livr es avec 1 Atelier B Le manuel donne une description complete de ces machines le lecteur d
28. able var de type article dont le premier champ tab est de type tableau d entiers dont les index sont entre 4 et 12 et le deuxi me champ valid est de type bool en on crira CONCRETE_CONSTANTS type_tableau type_article PROPERTIES type_tableau 4 12 gt INT extension BO HIA amp type_article struct tab type_tableau valid BOOL extension BO HIA VALUES type_tableau 4 12 gt INT inutilis par le traducteur type_article struct tab type_tableau SP CIFICIT S DU LANGUAGE BO ACCEPT PAR LE TRADUCTEUR HIA 45 valid BOOL inutilis par le traducteur CONCRETE VARIABLES var INVARIANT var type article typage explicite par identificateur impos par BO HIA INITIALISATION var rec 4 12 41 FALSE B 4 Param tres formels Les param tres formels effectifs sont traduits directement dans le paquetage de l instance concern e Par exemple si Mch est un composant B poss dant un param tre formel scalaire param et que dans le projet on cr e deux instances i1 Mch 5 et i2 Mch 10 de mch alors dans le paquetage i1_Mch on d finit une constante param de valeur 5 dans le paquetage i2_Mch on d finit une constante param de valeur 10 Les param tres formels effectifs sont donc d clar s dans les paquetages associ s Par cons quent ils ont la port e de ces paquetages Supposons maintenant qu un composant Mch
29. cibld Dans sa version 4 6 le code produit par ce logiciel a t test avec un compilateur GNU dans les environnements suivants Station de travail Sun sous Solaris 2 5 1 Station de travail Sun sous Solaris 2 6 Station de travail HP sous HP UX 10 20 Micro ordinateur type PC sous Linux 2 2 Cette fonctionnalit permet d int grer un projet crit en langage cible la traduction des l ments s curitaires r alis s en B 20n peut ainsi r aliser une activit de traduction crois e 6 Traducteurs de l Atelier B Manuel Utilisateur Remarque importante L utilisateur doit poss der un environnement de d veloppement pour le langage cible complet aucun outil de compilation ou d interpr tation du langage cible n tant livr avec le Traducteur 2 3 Services offerts 2 3 1 Pr ambule Motivation de la traduction en deux passes Cette section pr sente des aspects techniques qui peuvent tre ignor s dans un premier temps par un utilisateur d butant qui peut alors se rendre directement au paragraphe Le Traducteur permet de traduire automatiquement toute impl mentation BO en langage cible Une impl mentation BO n est pas traduite en un code source en langage cible en un seul appel ou une seule passe du traducteur On utilise deux passes la traduction unitaire au cours de cette premi re passe chaque impl mentation BO est traduite en un fichier objet ind pendament
30. cuting home ada bed bed s tmp blka04747 i home B projet lang makefile blf o home B projet lang makefile VM MM NNN NNN NN NNN Vo VV Vo VoVoYV Executing rm tmp blka04747 Freeing allocated objects VM VM ve ADA translation successful 3 1 3 Utilisation du Traducteur en ligne Le chapitre 5 pr sente les options d utilisation offertes lors de l utilisation du Traducteur Ce sont elles qui doivent tre utilis es si l on veut effectuer des traductions en ligne Remarquons que cette possibilit doit tre r serv e des utilisateurs exp riment s car 5L exemple donn est produit par le Traducteur Ada la sortie est similaire pour les autres traducteurs 6L exemple donn est produit par en mode verbeux Par d faut on obtient une sortie plus concise 14 Traducteurs de l Atelier B Manuel Utilisateur Traducteur Logiciel Ada tbada HIA tbhia C tbcpp C tbcpp c F1G 3 2 Traduction d une implementation depuis la ligne de commande Lors de l utilisation en ligne il faut fournir de nombreux param tres r pertoires base de donn es projet bdp et traduction lang chemin d acc s de l diteur de liens outil bed r pertoire contenant les informations du projet LIBRARY Si on utilise le Traducteur en ligne il faut g rer la main la coh rence des fichiers Ainsi si les fichiers sources B sont modifi s il ne faut pas oublier d
31. des autres impl mentations Ces fichiers objets produits par la premi re passe peuvent tre r utilis s par plusieurs projets permettant ainsi la cr ation de biblioth ques B l dition de liens au cours de cette seconde passe le Traducteur produit notamment les fichiers en langage cible se reporter au paragraphe 2 3 3 Ces fichiers en langage cible sont li s au projet en cours et ne peuvent pas tre r utilis s dans un autre projet Les motivations de ce m canisme de traduction en deux passes production des fichiers objets puis dition de liens sont li es aux objectifs suivants du Traducteur Traduction complete de l ensemble du langage BO Traduction fidele et performante Traduction compl te de l ensemble du langage BO Un certain nombre de problemes de conflits d identificateurs peuvent survenir lors de la traduction de B0 en langage cible Le langage BO distingue les identificateurs ident et IDENT ce qui n est pas le cas du langage Ada L identificateur void en BO entre en collision avec le mot clef r serv void en C Le langage BO autorise l criture d identificateurs comportant plus d un caract re _ la suite comme par exemple ident__ificateur Ces identificateurs ne sont pas des identificateurs Ada valides Certains identificateurs BO valides entrent en conflit avec le langage cible Par exemple package est un identificateur BO valide Ainsi il est clair qu un
32. e l utilisation du logiciel et doit permettre une prise en main progressive et compl te du Traducteur Lorsqu il sera familiaris avec le logiciel l utilisateur averti trouvera dans le chapitre 5 un r sum des options d utilisation du Traducteur 1 5 Conventions et syntaxe Les objets informatiques tels que les noms de fichiers de fen tre ou les choix d op tions dans les menus sont cris au moyen d une police non proportionnelle comme dans l exemple ci dessous La machine MM mch Les changes d entr es sorties entre l utilisateur et le logiciel sont d crits au moyen de la m me police Pour diff rencier les entr es des sorties les messages produits par le logiciel seront pr c d s du signe gt comme dans l exemple ci dessous ls gt AA mch AA 1 imp SCCS Les mots dont la signification est expliqu e dans le glossaire chapitre 6 page 35 sont suivis d une ast risque comme dans l exemple suivant L utilisateur de PIAM Les paragraphes d crivant les sp cificit s d un ou plusieurs traducteurs seront pr c d s du signe et crits dans une police sp cifique comme ceci 9 CETTE SECTION NE CONCERNE PAS LE TRADUCTEUR DESCRIPTION DU MANUEL 3 1 6 Documents associ s La bibliographie page HH donne une liste d ouvrages qui permettent l utilisateur d butant de se former l utilisation de l Atelier B et du langage cible et qui servent de r f rence l u
33. e leur faire passer les tapes de v rification de BO Le tableau 3 2 donne le nom de chaque traducteur Dans les exemples suivants nous consid rerons un projet B Mon_Projet que l on veut traduire en C On doit alors conna tre les informations suivantes identificateur signification Mon_Projet lang Chemin d acc s au r pertoire de traduction Mon_Projet spec Chemin d acc s aux sources B AB press lib Chemin d acc s au projet LIBRARY fourni avec l Atelier B Entree Le point d entr e du projet 1 Cas d une traduction unitaire Traduction de implantation Component 1 imp du projet Mon_Projet tbcpp i Component_1 imp P Mon_projet lang I AB press lib spec L AB press lib lang cpp w 2 Cas de la traduction du point d entr e du projet avec dition des liens Traduction du point d entr e Entree_1 imp et dition des liens tbcpp o Mon_Projet e Entree E bed P Mon_Projet lang I AB press lib spec L AB press lib lang cpp w Cet exemple ne remplace pas la lecture du chapitre 5 qui donne la liste compl te des services 3 1 4 Compilation et ex cution du code produit Ex cution sur la machine qui h berge Atelier Il suffit dans une fen tre shell de se placer dans le r pertoire lang du projet et de taper make Ex cution sur une machine cible Il faut transf rer sur cette machine le contenu complet du r pertoire lang du projet
34. e phase de r solution des conflits d identificateurs globale un pro jet est n cessaire afin de r aliser une traduction automatique et syst matique du langage BO en langage cible PR SENTATION DU LOGICIEL 7 Traduction fidele et performante 9 CETTE SECTION NE CONCERNE PAS TRADUCTEUR HIA QUI GERE DIFF REMMENT LA TRADUCTION DES TABLEAUX ET DES ARTICLES VOIR L ANNEXE B POUR PLUS DE D TAILS La traduction fidele des tableaux B0 impose de d terminer par inf rence les types des ta bleaux utilis s et de g n rer automatiquement les types tableaux associ s Cette gestion doit tre performante car deux tableaux qui ont le m me type inf r en BO doivent tre traduits par deux tableaux qui ont le m me type g n r en langage cible afin par exemple de pouvoir copier et comparer ces tableaux Le m me probl me se pose lors de la traduction des articles BO il faut inf rer une d claration du type article associ Une phase de g n ration et de r solution des types tableaux et articles globale au projet est donc n cessaire la traduction fid le et performante des l ments de ce type du langage BO qui ne type pas les tableaux et les articles vers le langage cible C C ou Ada qui impose une d claration explicite des types tableaux et articles R solution des collages implicites et du renommage La r solution des collages implicites et des renommages dans un langage fortement typ comme Ada ou C
35. e point d entr e du projet On appuie sur le bouton Translator et on choisit le langage cible avec Language et A11 pour Components Le nom du module de lancement point d acc s produit est le nom du projet B Le paragraphe donne un exemple des messages produits par le Traducteur Ada au cours de la traduction 3 1 2 Utilisation du Traducteur au moyen du mode batch Traduction d une impl mentation BO Pour traduire une impl mentation implementation_1 imp d un projet proj au moyen du mode batch de l Atelier B il faut taper la commande donn e par la table 3 1 Le Traducteur P produit alors une sortie du type suivant gt gt Translating into ADA the file implementation_1 gt Entering BO gt Ada mode gt Creating B Extended Tree gt Creating package specifications home B projet lang implementation str gt Creating package body home B projet lang implementation bod gt Creating B Link file home B projet lang implementation blf gt Free B Extended Tree gt gt gt Translation into ADA successful Si Von r it re la commande sans changer le fichier source BO on obtient un message du type gt Component implementation_1 is already translated 2Les op rations de cr ation et de gestion de projet ne sont pas d crites dans ce manuel le lecteur trouvera leur description dans ATB1 3L exemple donn est produit par le Traducteur Ada la sortie est similaire pour les autres traducteurs
36. e prend en entr e un param tre this de type T_P x puis autant de param tres en entr e que de param tres formels de type scalaire ou ensembliste La figure 2 donne la correspondance entre les types BO et les types C Une fonction T_P_INITIALISATION Elle prend en entr e un param tre _this de type T_P Elle d crit Vinitialisation de l instance Autant de fonctions que d op rations de la machine Ces fonctions ont le nom que l op ration dans la sp cification B pr fix du nom de la pseudo classe et pr c d du nom de la machine lui m me encadr par des caract res i e selon le format machine T_P_operation On obtient leurs param tres de la fa on suivante Le premier param tre est this de type T_P x Les param tres d entr e de l op ration dans l ordre de leur d claration en B Les types sont obtenus conform ment au tableau de la figure Suivent ensuite les param tres de sortie de l op ration dans l ordre de leur d claration en B Les types sont obtenus conform ment au tableau de la figure A 2 A 4 5 Le fichier B Link File Le fichier B link File est compos de plusieurs sections d limit es par les mots cl s _BEGIN_NOM_SECTION et _END_NOM_SECTION Ces sections peuvent tre vides ou absentes Elles contiennent des informations permettant de g rer les conflits de noms lors de l dition de liens entre les diff rents modules ainsi que les conflits avec le langa
37. emple le systeme cible est iden tique au syst me de d veloppement ce sont tous deux des syst mes Unix le langage cible choisit est l Ada et on utilise le compilateur Ada gnat On se place dans le r pertoire o les fichiers sont traduits et on tape make La figure 4 6 donne un exemple d affichage obtenu Avertissement La traduction de ce projet avec le traducteur fourni avec la version 3 6 de l Atelier B conduit une erreur du traducteur On peut alors lancer l ex cution du projet La figure pr sente le r sultat de cette ex cution 4 2 D veloppement d un projet h t rog ne B Langage cible CETTE SECTION NE S APPLIQUE PAS AU TRADUCTEUR HIA QUI COMPORTE DES SP CIFICIT S D CRITES AU PARAGRAPHE Tout comme un projet autonome un projet h t rog ne doit comporter un point d entr e Le point d entr e est un composant logiciel appel paquetage en Ada ou module en C C qui permet de cr er les instances physiques des composants et de les initialiser correctement Il permet ensuite d acc der toutes ces instances Il exporte une proc dure INITIALISATION et selon le langage cible SC NARIOS D EXPLOITATION 27 DEBUT DU TEST Affichage de la pile vide Resultat attendu PILE VIDE Resultat effectif la pile est vide On remplit la pile puis on l affiche Resultat attendu PILE PLEINE Resultat effectif fond de la pile 1 2 3 haut de la pile On vide la pile puis on l
38. fiche_pile_1 pile_1 FIG 4 5 Graphe de d pendance du projet 4 1 4 Int gration des composants dans l Atelier B Le lecteur se r f rera au document pour avoir des explications d tailll es sur l int gration de composants dans Atelier B Ce paragraphe se borne lister succintement les tapes suivre Ainsi l utilisateur doit effectuer les op rations suivantes Cr er un projet Dans la suite de ce chapitre nous supposerons que le nom du projet est DEMO_PILES Attacher ce projet la biblioth que LIBRARY Le projet aura ainsi acc s la machine de base BASIC_I0 Ins rer les composants d taill s au paragraphe 1 1 3 Effectuer les tapes de Type_Check puis de BO Check sur ces composants POUR LE TRADUCTEUR HIA L TAPE DE BO CHECK NE DOIT PAS TRE R ALIS E R aliser la preuve de ces composants Si cette tape n est pas obligatoire pour pouvoir r aliser la traduction en lanage cible elle est la seule garante de qualit du code produit Le r sultat de la traduction d un code non prouv 100 n est pas garanti 4 1 5 Traduction unitaire du code cible produit On s lectionne les quatre impl mentations du projet et on appuit sur Translator Dans la fen tre qui appara t on choisit le langage cible et Selected Only 4 1 6 Edition des liens du projet On s lectionne l impl mentation demo_1 et on appuit sur Translator Dans la fen tre qui appara t on choisit
39. ge cible Elles per mettent aussi de r pertorier les types tableaux et les constantes export es par le module Si on suppose que le code de la machine de base est un code correct utilisant des iden tificateurs valides pour le langage cible choisi il suffit d indiquer le nom de la machine section CLASS et de remplir la section des noms des op rations export es par la machine sous section LEVEL_1 de la section CLASS Ainsi les noms des op rations export es par la machine de base n entreront pas en conflit avec des noms d autres modules ATTENTION POUR LES TRADUCTEURS ADA ET HIA ET CONTRAIREMENT AUX CONVEN TIONS DU LANGAGE ADA LE NOM DES OP RATIONS DOIT RESPECTER L UTILISATION DES MAJUSCULES ET DES MINUSCULES QUI EST FAITE DANS LE SOURCE B DE LA SP CIFICATION DE LA MACHINE DE BASE La figure donne l exemple du fichier B Link File fourni pour la machine de base BASIC IO Les classes T_set et T_array_X sont d finies dans des composants pr d finis fournis avec le traducteur 42 Traducteurs de l Atelier B Manuel Utilisateur RSS A Off ff ta Base machine BASIC IO for ADA target language C 2001 ClearSy Version basic_io blf 1 2 date 22 Mar 1996 RSS A Off ft BEGIN CLASS Machine name BASIC IO BEGIN LEVEL 1 Class level operations INTERVAL READ INT WRITE BOOL READ BOOL WRITE CHAR READ CHAR WRITE STRING WRITE END LEVEL 1 END CLASS FIG A 3
40. heques utilis es et ce dans l ordre de leur d claration Cas d un projet h t rogene Dans le cas d un projet h t rog ne le service d dition des liens prend en entr e le nom de la sp cification d une impl mentation destin e tre le point d entr e d un projet ainsi que le nom d un module de lancement cr er et produit L ensemble des fichiers sources interfaces et corps des composants du projet Le code cible du point d acc s au projet B Ce module permet d initialiser ensemble des composants B puis d acc der l ensemble des donn es et des op rations de ces machines L interface et le corps du module sets en ADA ou SETS en C C pour les types ta bleaux inf r s les constantes concr tes les ensembles abstraits et les pr d finis succ pred MAXINT MININT Un squelette de fichier makefile permettant de g n rer le projet L diteur de liens parcourt r cursivement les liens d importation de cette machine et tra duit ainsi en code cible terminal l ensemble des fichiers objets utilis s par le projet Les fichiers objets sont recherch s dans le r pertoire lang du projet en cours de traduc tion puis dans les r pertoires lang des biblioth ques utilis es et ce dans l ordre de leur d claration Remarque importante les biblioth ques doivent tre traduites avant le projet qui le uti lise Si ce n est pas le cas l dition des liens du projet choue
41. ie ces valeurs il doit s assurer Que la taille maximum de ligne qu il fournit n exc de pas les capacit s de son compilateur cible Que la taille maximum de ligne qu il fournit n emp che pas la g n ration du code En effet les appels d op ration sont pr fix s par les noms de machines qui les d finissent On voit que l on peut ais ment provoquer une g n ration de lignes ins cables longues en donnant des noms longs aux machines et aux op rations Il faut veiller alors la compatibilit entre ce choix et le choix de la taille maximale des lignes produites L outil V rificateur aux limites de l Atelier B peut aider l utilisateur fixer ces limites PRINCIPES D EXPLOITATION 17 3 3 4 Compatibilit du Traducteur avec l Atelier B Il faut toujours veiller disposer d une version du Traducteur compatible avec les outils de Atelier B 3 3 5 Nommage des modules et des projets dans le cas des Traducteur Ada et HIA CETTE RESTRICTION NE CONCERNE QUE LES TRADUCTEURS ADA ET HIA Les seuls conflits de noms que l diteur de liens ne peut pas r soudre sont les conflits qui surviennent dans les noms de modules En effet l diteur de liens ne peut pas renommer les modules car le langage Ada impose que les fichiers qui repr sentent une unit de compilation i e une proc dure ou un paquetage aient le m me nom que cette unite Par exemple si un nom de module ou de projet est en conflit avec un mot
42. it avoir pass avec succ s l tape de v rification de BO pour pouvoir tre traduit 9 CETTE TAPE N EST PAS R ALIS E POUR LE TRADUCTEUR HIA QUI INTEGRE NATI VEMENT UN MODULE DE V RIFICATION DU LANGAGE BO QUI LUI EST PROPRE Ainsi si cette tape n a jamais t effectu e ou si le composant a t modifi depuis la derni re v rification l outil de v rification de BO est tout d abord appel sur l impl mentation traduire Cet outil peut son tour provoquer l appel du Type Checker sur cette impl mentation Si besoin est les machines vues sont galement analys es par cet outil Le paragraphe donne un exemple des messages produits par le Traducteur Ada au cours de la traduction ILes op rations de cr ation et de gestion de projet ne sont pas d crites dans ce manuel le lecteur trouvera leur description dans ATB1 11 12 Traducteurs de l Atelier B Manuel Utilisateur Traducteur Commande Ada adatrans implementation 1 HIA hiatrans implementation 1 C ctrans implementation_1 C c trans implementation 1 Fig 3 1 Traduction d une implementation en mode batch On peut de la m me fa on r aliser la traduction de plusieurs impl mentations en une seule op ration en les s lectionnant toutes dition des liens globale au projet Pour r aliser une dition des liens globale un projet on s lectionne au moyen de la souris le fichier qui sert d
43. loppement Cepen dant la traduction d un composant non encore prouv provoque l mission d un message d avertissement et le code g n r comporte dans son ent te un commentaire d avertisse ment En effet le code g n r peut ne pas tre compilable cas d une erreur de conception en B qui ne se d tecte qu la preuve soit lever des exceptions au cours de son ex cution cas par exemple d un acc s un index invalide d un tableau 3 3 2 Avertissement important relatif aux valeurs des constantes MAXINT et MININT Le Traducteur Ada permet de red finir les valeurs de MAXINIT et de MININT afin de pouvoir traduire du code destin un syst me cible dont l architecture diff re de celle du syst me h te L utilisation d une valeur de MAXINT et ou de MININT diff rente de celle employ e par le prouveur provoque un r sultat non garanti Par d faut le Traducteur est compatible avec le prouveur Il est recommand de prendre conseil aupr s de ClearSy si vous souhaitez modifier les valeurs de ces constantes 3 3 3 Taille des lignes produites Certains compilateurs cible n admettent en entr e que des fichiers dont les lignes ne d passent pas une certaine taille Ainsi le Traducteur contr le la longueur des lignes qu il produit Cette longueur est pa ram tr e par l utilisateur au moyen des options 1 et t et dont les valeurs par d faut respectives sont 80 et 4 Si l utilisateur modif
44. mp i e selon le format machine operation On obtient leurs param tres de la fa on suivante Les param tres d entr e de l op ration dans l ordre de leur d claration en B Les types sont obtenus conform ment au tableau de la figure Suivent ensuite les param tres de sortie de l op ration dans l ordre de leur d claration en B Les types sont obtenus conform ment au tableau de la figure A 2 A 4 4 M thode d criture de code cible en C CETTE SECTION NE S APPLIQUE QU AU TRADUCTEUR C Le nom de la pseudo classe est le nom de la sp cification B pr fix e par T_ Soit P ce nom C est en fait une structure laquelle on accede uniquement aux travers de fonctions pr fir es par le nom de la classe qui mulent les m thodes d une v ritable classe Les classes T_set et T array X sont d finies dans des composants pr d finis fournis avec le traducteur LES MACHINES DE BASE 41 La pseudo classe T _P doit d finir Un champ initialisation de type T_bool Un champ par donn es n cessaires la mod lisation de la machine param tre formel variable concr te Les noms des champs sont pr fix s par le nom de la machine entre caract res Les m thodes de la classe Tp sont mul es par les fonctions suivantes Une fonction new_T_P C est l quivalent du constructeur de la classe Elle prend en entr e un param tre this de type TP x Une fonction T_P_IMPORTS Ell
45. mple la pile est implant e sur un tableau statique de 10 entiers Le composant offre deux op rations empiler et depiler qui permettent de g rer la pile La figure donne le code source B de la sp cification et de l impl mentation de ce composant POUR TRADUIRE EN HIA IL FAUT D FINIR UN TYPE TABLEAU EXPLICITE type_tableau 1 10 gt NAT ET UTILISER CE TYPE POUR TYPER la pile Le composant affiche_pile Le composant affiche_pile permet d afficher une pile au format d fini par le compo sant pile c est dire une pile implant e sur un tableau de 10 l ments Ainsi l op ration affiche qui permet d afficher une pile prend en param tre non seulement le tableau qui repr sente la pile mais galement la taille courante de la pile i e le nombre d l ments du tableau qui font partie de la pile Pour des raisons de pr sentation cette op ration prend galement en entr e un message afficher avant d afficher la pile La figure donne le code source B de la sp cification et de l impl mentation de ce composant POUR TRADUIRE EN HIA IL FAUT D FINIR UN TYPE TABLEAU EXPLICITE type tableau 1 10 gt NAT ET UTILISER CE TYPE POUR TYPER pile LES AUTRES COMPOSANTS par exemple pile DOIVENT TYPER LEURS PILES AVEC type tableau POUR QUE LA TRADUCTION FONCTIONNE Le composant interface pile Le composant interface pile offre un niveau d abstraction sup rieur aux deux compo sants pr c dents Il est param
46. n re du code dont l ex cution produit des traces sur les op rations appel es et les valeurs des param tres v Mode verbeux V Num ro de version et usage du logiciel w Ajoute le message composant non prouv au code g n r utilis automatiquement par l Atelier FIG 5 2 Options utilisables lors de la traduction unitaire d un composant L option T du Traducteur Ada permet d effectuer une traduction du projet avec des traces Cette option permet Au niveau d une traduction unitaire de demander une traduction d un module avec production de traces Au niveau de l dition des liens de demander l ajout des modules de trace lors de la compilation Un projet qui a t traduit avec des traces produit lors de son ex cution une trace compl te des appels de fonction Cette trace est produite dans le fichier trace situ dans le r pertoire d o le projet est lanc Dans ce fichier on r pertorie Les appels de fonction avec affichage de l instance implicite ainsi que de la valeur des param tres en entr e Les retours de fonction avec affichage de l instance implicite ainsi que de la valeur des param tres en sortie Ainsi une traduction avec des traces permet l utilisateur de suivre pr cis ment le d roulement de son projet sans avoir rajouter pour cela des instructions dans son code source B LISTE COMPLETE DES SERVICES 33
47. nsembles par les traducteurs fournis avec l Ate lier B est parfois incorrecte Il est d conseill d utiliser le m me nom pour diff rents param tres formels ensembles Utilisation des composants r utilisables Les composants r utilisables fournis avec l Atelier B utilisent des param tres formels en semble Cons quence de l anomalie pr cit e leur utilisation avec les traducteurs ADA C et C peut aboutir sur une erreur du traducteur ou une code cible erron qui ne peut donc pas s ex cuter Chapitre 6 Glossaire API Application Program Interface Interface ext rieure offerte par un syst me ou une bibliotheque Code offensif Un code offensif est un code o l on suppose que l utilisateur respecte un contrat i e que certaines conditions sont respect es Ainsi on ne teste pas ces conditions dans le code En C les fonctions du type strcpy et strcmp sont des exemples de code offensif car elles ne v rifient pas l int grit de leurs arguments zones m moires allou es par Vutilisateur chaines termin es par NO IHM Interface Homme Machine Cette interface est graphique l interface en mode texte par ligne de commande est le mode batch Mode batch Mode de fonctionnement par ligne de commande de Atelier B Ce mode permet d ex cuter des proc dures automatiques d crites sous formes de fichiers de commandes SCCS Source Code Control System Ensemble d outils permettant de g rer l
48. odes de fonctionnement 11 q 1 EEE 12 o TOS E Bosco GR VB E aj a A q 13 3 1 4 Compilation et ex cution du code produitl 14 3 2 Les entr es et sorties 15 A a En E 15 bp nes 15 SF 15 3 2 4 Les fichiers 15 D de A a D D Ut E 16 ii TABLE DES MATIERES 3 3 1 Avertissement important relatif a la preuvel 16 Ne ia EE SR TRS MR E a 16 RS SO He o SR la De E ne 16 de ds 17 RE RN vet da AR a i 17 19 e A ie one 19 UE aa Pa 19 Roi SR E a RE SR RS 19 o A 20 4 1 4 Int gration des composants dans l Atelier B 25 4 1 5 Traduction unitaire du code cible produit 25 4 1 6 Edition des liens du projet 25 ns 26 4 2 D veloppement d un projet h t rog ne B Langage cible 26 4 3 D veloppement d un projet h t rog ne B HIA 28 31 E RARA AN 31 5 2 Edition des liens d un projet 31 aa AAA Aa 31 e ER a a e aa Rr ES de 34 35 37 te q PR VE 37 O aAa aa a oa ER Ea 37 Sa e Aa pea a ESA O y ESA ra E SEU 37 TEET 37 a a a 38 Rs e a ai e A 38 A 4 M thode d criture du code cible sp cification et corps 38 Si a os 39 D ol a A E E 39 NA Y ar 40 A44 M thode d criture de code cibleenCl 40 TABLE DES MATIERES iii e a ia Baca 41 43 as a AO RA RUE e a e 43 a
49. s 8 Traducteurs de l Atelier B Manuel Utilisateur Langage cible Apr s traduction Apr s dition de liens Ada mach str mach ads HIA mach str mach ads C mach spe mach h C mach spe mach h Fig 2 1 Fichiers produits pour l interface de mach Langage cible Apr s traduction Apr s dition de liens Ada mach bod mach adb HIA mach bod mach adb C mach bdy mach c C mach bdy mach cpp FIG 2 2 Fichiers produits pour le corps de mach correspodant l utilisation des composants dans le projet B traduire 2 3 2 Service de traduction automatique d une impl mentation BO en langage cible Ce service prend en entr e une impl mentation BO mach imp et produit les fichiers sui vants Deux fichiers pour l interface de mach Un apr s traduction et un apr s dition de liens Les noms des fichiers sont donn es par le tableau Deux fichiers pour le corps de mach Un apr s traduction et un apr s dition de liens Les noms des fichiers sont donn s par le tableau Un fichier objet qui d crit les symboles import s et export s par mach Par d faut de fichier est nomm mach blf Ce fichier permet entre autres de produire la liste des substitutions appliquer sur les fichiers objets d interface et de corps afin de produire les fichiers cible finaux 2 3 3 Service d dition des liens Cas d un projet autonome
50. s en C C ou Ada en Ada un objet this en C un objet entry en C une structure entry La proc dure INITIALISATION permet de cr er les instances physiques et this entry permet de r f rencer les objets du projet Ainsi this entry r f rence l instance du point d entr e du projet i e Vinstance de demo dans notre exemple et ensuite on peut parcourir r cursivement le graphe de d pendance du projet en appliquant la r gle suivante Si on atteint l instance 1 du graphe gr ce au chemin A Sil utilisd une instance J Alors on atteint l instance J par le chemin A ref Jen Ada ou ref_J en C C Ainsi en se r f rant au graphe de d pendance illustr par la figure 4 5 de la page on peut construire une table qui associe chaque instance physique du projet un chemin d acc s La figure pr sente cette table pour notre exemple On peut alors appeler les op rations des composants sans oublier de leur passer en pre mier argument le param tre d instance implicite i e le pointeur qui permet de les at teindre Ainsi on peut appeler la m thode affiche du composant affiche_pile cr e par interface_A en crivant le code suivant Langage Code Ada affiche pile affiche this ref interface A ref affiche pile C affiche_pile gt affiche entry gt ref_interface_A gt ref_affiche_pile C entry interface_ A affiche_ pile affiche 4
51. scules encadr par des caract res i e selon le format machine operation On obtient leurs param tres de la fa on suivante Le premier param tre dit d instance implicite de type TYPE_P qui pointe sur l instance du composant sur laquelle on effectue l op ration Suivent ensuite les param tres d entr e de l op ration dans l ordre de leur d claration en B Ce sont des param tres de mode in Les types sont obtenus conform ment au tableau de la figure Suivent ensuite les param tres de sortie de l op ration dans l ordre de leur d claration en B Ce sont des param tres de mode in out Les types sont obtenus conform ment au tableau de la figure A 4 2 M thode d criture de code cible en HIA CETTE SECTION NE S APPLIQUE QU AU TRADUCTEUR HIA 40 Traducteurs de l Atelier B Manuel Utilisateur Le nom du paquetage est le m me que le nom de la sp cification B en utilisant in diff remment des majuscules ou des minuscules Par contre les noms de fichiers utilis s doivent tre en minuscules Soit P ce nom Le paquetage P doit d finir Une clause with pour chaque machine requise La traduction de la proc dure INITIALISATION plac e dans la fonction d initilisation du paquetage Autant de proc dures que d op rations de la machine Les proc dures ont le m me nom que dans la sp cification B pr c d du nom de la machine en minuscules encadr par des carac
52. souhaitera diff rencier ces logiciels on crira explicitement le Traducteur Ada le Traducteur HIA le Traducteur C ou le Traducteur C De la m me mani re lorsque l on fera r f rence au langage cible cela signifiera que l on voque le langage Ada HIA C ou C Le but du manuel utilisateur est de mettre les connaissances requises la disposition des personnes amen es faire fonctionner le Traducteur Il poursuit un double objectif permettre ces personnes de se former de fa on progressive leur servir de r f rence pour identifier les comportements de ces logiciels Pour ce faire on expose les connaissances pr requises la fa on de consulter le manuel selon le besoin de l utilisateur les conventions d criture utilis es et les lectures utiles 1 2 Connaissances pr requises La lecture de ce manuel suppose que l utilisateur soit form au langage B et au langage cible ainsi qu l utilisation de PV Atelier B et du compilateur cible lLe traducteur Ada traduit l ensemble des impl mentation BO en code Ada conforme aux normes Ada 83 ADA 83 et Ada 95 ADA 95 2Le traducteur HIA produit du code High Integrity Ada syntaxiquement conforme la norme SPARK d crite dans SPARK En contrepartie de quelques restrictions sur le langage BO en entr e il g n re un code plus simple tr s proche du BO et plus s curitaire 3Ce traducteur traduit l ensembe des impl mentations en code
53. t crit les fichiers en utilisant 1 APT standard du syst me d exploitation Les points surveiller sont donc V rifier que l utilisateur qui lance le logiciel a les droits suivants droit de lecture dans les r pertoires de source et bdp du projet des biblioth ques utilis es et pour tous les fichiers de ces r pertoires droit d criture dans les r pertoires lang et bdp du projet V rifier que le syst me de fichiers du projet n est pas plein Si ces consignes ne sont pas respect es le Traducteur produit un message d erreur expli citant le probl me d au syst me Ces messages sont fournis au logiciel par le syst me Il peut donc tre n cessaire de configurer le syst me ou le compte de l utilisateur pour modifier les caract ristiques de ces messages la langue utilis e par le syst me pour fournir les messages d erreurs peut parfois tre param tr e par des variables d environnement ou par d autres m thodes TOn utilise le traducteur HIA dans cet exemple 16 Traducteurs de l Atelier B Manuel Utilisateur 3 3 Pr cautions d emploi 3 3 1 Avertissement important relatif a la preuve Le code cible g n r par le Traducteur n est valide que si les composants qui sont traduits sont compl tement prouv s Le Traducteur permet de traduire des projets dont les composants ne sont pas compl tement prouv s afin d offrir aux utilisateurs plus de souplesse dans leur d ve
54. t res i e selon le format machine operation On obtient leurs param tres de la fa on suivante Les param tres d entr e de l op ration dans l ordre de leur d claration en B Ce sont des param tres de mode in Les types sont obtenus conform ment au tableau de la figure Les param tres de sortie de l op ration dans l ordre de leur d claration en B Ce sont des param tres de mode in out Les types sont obtenus conform ment au tableau de la figure A 4 3 M thode d criture de code cible en C CETTE SECTION NE S APPLIQUE QU AU TRADUCTEUR C Le nom de la classe est le nom de la sp cification B prefix e par T_ Soit P ce nom La classe T _P doit d finir la classe T_P qui doit comporter obligatoirement un champ initialisation de type T bool Dans cette classe on place toutes les structures de donn es n cessaires la mod lisation des instances de chaque machine Une fonction membre IMPORTS qui d crit l instance importer puis autant de pa ram tres en entr e que de param tres formels de type scalaire ou ensembliste La figure A 2 donne la correspondance entre les types BO et les types C Une fonction membre INITIALISATION qui d crit l initialisation de l instance Autant de fonctions membre que d op rations de la machine Les proc dures ont le m me nom que dans la sp cification B pr c d du nom de la machine en minuscules encadr par des caract res a
55. tilisateur averti Traducteurs de l Atelier B Manuel Utilisateur Chapitre 2 Pr sentation du logiciel 2 1 Mission La mission du logiciel Traducteur est de r aliser une traduction automatique des impl mentations BO d un projet en code source cible Le code cible produit peut soit tre compil afin de r aliser un projet ind pendant soit tre int gr un d veloppement en langage cible natif Le Traducteur est capable de traduire en langage cible l ensemble du langage BO Il n y a aucune restriction notamment en ce qui concerne le nommage des identificateurs les ventuels identificateurs qui entreraient en conflit avec le langage cible sont renomm s par le traducteur Remarque importante le traducteur HIA travaille sur la base d un language BO qui poss de quelques sp cificit s qui sont d taill es dans l annexe B Ainsi tout composant qui est analys avec succ s par le v rificateur de BO peut tre traduit en langage cible Dans la suite de ce manuel on appellera impl mentation BO toute impl mentation de composant pour laquelle le v rificateur de BO s ex cute avec succ s 2 2 Environnement recommand Le Traducteur est destin tre ex cut sur les m mes plate formes que l Atelier B Le Traducteur g n re un code cible portable conforme aux normes en vigueur Des options du logiciel permettent de param trer le code g n r pour s adapter au syst me et au compilateur
56. uelettes obtenus par le code souhait A 3 1 M thode d criture de la sp cification B La sp cification B est crite en suivant les r gles usuelles de l criture d un composant en B Il est int ressant d crire une sp cification qui d crit aussi pr cis ment que possible l effet des op rations de la machine de base plut t que de se limiter donner des coquilles vides i e skip pour sp cification Ainsi le m canisme de preuve permet de garantir l auteur du code en langage cible de la machine de base qu un certain nombre de contraintes son respect es et donc d crire du code offensif A 4 M thode d criture du code cible sp cification et corps Le code cible doit tre compos d une sp cification et d un corps de paquetage localis dans deux fichiers Les extensions respectives par d faut de ces deux fichiers sont donn es par la table 5 2 Si l on utilise les options du Traducteur permettant de changer ces extensiond on veillera r percuter ce changement sur les suffixes des fichiers composant les machines de base Les paragraphes A 4 1 A 4 2 et explicitent les m thodes d criture de code cible pour les traducteurs Ada HIA C et C respectivement 2Ces options sont d crites au chapitre 5 LES MACHINES DE BASE 39 Type BO Type Ada HIA Type C C INT INTEGER T_int NAT INTEGER T_nat NAT 1 INTEGER T_nat BOOL BOOLEAN T_bool STRING STRING T_string
Download Pdf Manuals
Related Search