Mémoires soutenus dans le cadre du projet

" CONCORDE"

"un environnement de CONstruction, CORrection et DE transformation d'algorithmes."

"Environnement de construction, de test et de transformation d'automates".
"RÉCITE : Passage automatique d'algorithmes récursifs en algorithmes itératifs".
"Environnement de Construction & de test de D-algorithmes".
"Adaptation des algorithmes d'ARSAC et de RAMSHAW pour l'élimination des GOTO dans les B-algorithmes".
"Environnement de Construction & de test de R-algorithmes".
"Environnement de construction et de test de B-algorithmes.
"Environnement de construction et de test d'organigrammes". Application à l'entreprise.
"Environnement de preuves de R-algorithmes (algorithmes récursifs)".
"Environnement de preuves de D-algorithmes (algorithmes structurés)".
"Environnement de preuves de B-algorithmes (algorithmes à GOTO)".
Preuve des algorithmes récursifs par l’approche ‘Point fixe’.
Récursification des algorithmes procéduraux.
Évaluation des algorithmes procéduraux.

SUJET	"Environnement de construction, de test et de transformation d'automates"
PRÉSENTÉ PAR	B. ABASSI
On part du principe que tout algorithme est assimilé à un automate. L'expression d'un algorithme se fait donc de manière graphique, tel un automate avec ses états et ses fonctions de transitions. On a ainsi une liberté d'écriture d'algorithmes. Des outils sont offerts pour permettre à un utilisateur de : - de construire son automate. - de le tester. Dans la phase de test, nous pourrons voir au ralenti le passage d'un état à un autre, les valeurs que prennent les variables et les expressions. Des transformations remarquables ont été réalisées telles que le passage vers des b-algorithmes, des d-algorithmes et même des r-algorithmes. Des équivalents PASCAL correspondant à chaque type d'algorithmes ont été faits dans le but de confirmer la validité des transformations.

SUJET	RÉCITE : Passage automatique d'algorithmes récursifs en algorithmes itératifs"
PRÉSENTÉ PAR	H. SEBA
En se basant sur la sémantique de la récursion, l'algorithme récursif(r-algorithme) est transformé en b-algorithme, c'est à dire un algorithme informel utilisant uniquement les branchements conditionnels et inconditionnels. Le processus de passage peut être montré à l'utilisateur pour se rendre compte des différentes étapes de passage, notamment la traduction des appels récursifs et des retours de procédures. Afin de montrer que le passage du b-algorithme au r-algorithme est bien effectué, les deux types d'algorithmes ont été traduits en PASCAL et exécutés donc avant et après le passage.

SUJET	"Environnement de Construction & de test de D-algorithmes"
PRÉSENTÉ PAR	H. KHOUDOUR & S. GUEMACHE
Un D-algorithme est un algorithme structuré utilisant uniquement les structures de contrôle : Si ... Sinon ... Fsi et Tantque ..... Fintantque. Il s'agit d'assister l'utilisateur - pour écrire son D-algorithme. - pour tester son D-algorithme. Un module d'indentation a été aussi développé dans le but de rendre un algorithme plus clair et donc plus facile à lire.

SUJET	"Adaptation des algorithmes d'ARSAC et de RAMSHAW pour l'élimination des GOTO dans les B-algorithmes
PRÉSENTÉ PAR	F. BELGACEM & N. BERKANI.
Une adaptation des algorithmes de ARSAC et de RAMSHAW est réalisée. L'objectif est de pouvoir passer de tout algorithme exprimé uniquement avec les branchements conditionnel et inconditionnel vers un algorithme où les seules structures de contrôle utilisées sont l'alternative et la répétitive. Outre l'aspect pédagogique assigné à ce travail, une application réelle est réalisée. En particulier, Cette application est capable de structurer ( éliminer les GOTOs ) tout programme BASIC(ou FORTRAN)en y insérant éventuellement des commentaires.

SUJET	"Environnement de Construction & de test de R-algorithmes"
PRÉSENTÉ PAR	TOUIZ & OUHBA.
Un ensemble d'outils ont été développés dans le but d'assister l'utilisateur pour la construction de R-algorithmes et de lui permettre de dérouler son R-algorithme sur des données. L'aspect pédagogique pour expliquer le "mystère" de la récursivité est aussi abordé.

SUJET	"Environnement de construction et de test de B-algorithmes"
PRÉSENTÉ PAR	ZOUABER & BELGACEM
Un génie logiciel, ensemble d'outils, est développé afin , d'une part, d'assister l'utilisateur pour la construction d'algorithmes non structurés (B-algorithmes) c'est à dire des algorithmes exprimés avec les sauts conditionnels et inconditionnels. Et d'autre part afin de lui permettre de dérouler son algorithme sur des données concrètes. Une transformation de B-algorithmes en organigrammes est aussi réalisée.

SUJET	" Environnement de construction et de test d'organigrammes". Application à l'entreprise
PRÉSENTÉ PAR	S. SAOUD & Y. YALAOUI
Il s'agit de concevoir un éditeur, un interpréteur et un transformateur d'organigrammes. L'éditeur, en mode assisté, doit fournir tous les outils nécessaires pour la construction d'organigrammes (et de sous-organigrammes). L'interpréteur permettra le déroulement et donc le test( mise au point) des organigrammes en lui offrant des traceurs perfectionnés. Une transformation de l'organigramme en mode linéaire ( purement textuel) est réalisée. Une application directe du logiciel projeté serait la conception de systèmes via les organigrammes et la génération automatique des programmes associés ( Basic et/ou Pascal).

SUJET	" Environnement de preuves de R-algorithmes (algorithmes récursifs)"
PRÉSENTÉ PAR	M. BOUZARARI & F. REZOUG
Il s'agit de vérifier de manière automatique ( ou semi-automatique) la correction formelle d'un R-algorithme, c'est à dire un algorithme récursif avec uniquement l'alternative comme structure de contrôle. Afin d'établir cette preuve, on utilise la méthode de HOARE et les mécanismes de déductions de la logique des prédicats du premier ordre ( démonstration automatique de théorèmes) . Le logiciel développé a une retombée pédagogique. Outre toute la documentation nécessaire pour la compréhension de la preuve, le déroulement de celle-ci pourrait être montré pas à pas à tout utilisateur "curieux".

SUJET	" Environnement de preuves de D-algorithmes (algorithmes structurés)"
PRÉSENTÉ PAR	M.BOUKERROUI & O. TAHIR.
Il s'agit de vérifier de manière automatique ( ou semi-automatique) la correction formelle d'un D-algorithme, c'est à dire un algorithme où les seules structures de contrôle sont l'alternative et la répétitive. Afin d'établir cette preuve, on utilise les méthodes de HOARE et de DIJKSTRA et les mécanismes de déductions de la logique des prédicats du premier ordre ( démonstration automatique de théorèmes) . Le logiciel développé a une retombée pédagogique. Outre toute la documentation nécessaire pour la compréhension de la preuve, le déroulement de celle-ci pourrait être montré pas à pas à tout utilisateur "curieux".

SUJET	" Environnement de preuves de B-algorithmes (algorithmes à GOTO)"
PRÉSENTÉ PAR	H. LAICHOUR & F. ARRAR.
Il s'agit de vérifier de manière automatique ( ou semi-automatique) la correction formelle d'un B-algorithme, c'est à dire un algorithme où les seules structures de contrôle sont les branchements conditionnels et inconditionnels. Afin d'établir cette preuve, on utilise la méthode de FLOYD et les mécanismes de déductions de la logique des prédicats du premier ordre ( démonstration automatique de théorèmes) . Le logiciel développé a une retombée pédagogique. Outre toute la documentation nécessaire pour la compréhension de la preuve, le déroulement de celle-ci pourrait être montré pas à pas à tout utilisateur "curieux".

SUJET	Preuve des algorithmes récursifs par l'approche 'Point fixe'
PRÉSENTÉ PAR	M. AIMOUCHE
Tout algorithme récursif f peut être vu comme une équation de la forme f =µ (f) (où µ(f) désigne le corps de l'algorithme) admettant comme solution le plus point fixe de l'équation. Il s'agit de vérifier de manière automatique ( ou semi-automatique) la correction formelle d'un R-algorithme, c'est à dire un algorithme récursif avec uniquement l'alternative comme structure de contrôle. Afin d'établir cette preuve, on utilise la théorie du point fixe. Le logiciel développé a une retombée pédagogique. Outre toute la documentation nécessaire pour la compréhension de la preuve, le déroulement de celle-ci pourrait être montré pas à pas à tout utilisateur "curieux".

SUJET	Récursification des algorithmes procéduraux
PRÉSENTÉ PAR	H. GASMI, H. LAMRAOUI
Il s'agit de rendre récursif tout algorithme procédural ( à branchement(B), structurés(D), organigrammes(O) et automates(A) ). Une technique consiste, dans un premier temps, à représenter tout algorithme sous forme d'un système d'équation où les inconnues sont les étiquettes et de le "résoudre " dans un deuxième temps. La résolution engendre un ensemble de procédures récursives non paramétrées. Une paramétrisation des procédures est souhaitable. Dans le but d'ouvrir une voie vers les langages non procéduraux ( fonctionnels, logiques, ...) où la récursion est le mécanisme de base, une étude est faite sur la possibilité de minimiser, voir éliminer les affectations dans les programmes récursifs obtenus. L'outil développé a une retombée pédagogique.

SUJET	Évaluation des algorithmes procéduraux
PRÉSENTÉ PAR	M.AMRANI, M. RAHAL.
Une technique de vérification de programmes consiste à dérouler les programmes non pas sur des données concrètes mais sur des données abstraites. Il s'agit d'accepter des programmes à branchements (B), structurés( D) ou récursifs(R) en entrée et de les dérouler symboliquement, c'est à dire effectuer des opérations algébriques plutôt qu'arithmétiques, en vue de prouver leur correction. En d'autres termes, un calculateur d'opérations algébriques (simplification, mise en facteur, ...) est developpé puis intégré dans un système de preuve par évaluation symbolique. Le système projeté est impérativement interactif et a une retombée pédagogique.