Abstract FR:

Le but du travail est la proposition d'une methode systematique pour le developpement de logiciel fiable en partant de specifications algebriques. Nous introduisons un style intermediaire de specification que nous appelons specifications algebrico-operationnelles. Ce style permet la specification des operations au moyen des pre- et post-conditions qui sont obtenues par des techniques de transformations successives des axiomes de la specification algebrique. Cette specification intermediaire est le point de depart pour obtenir le code en appliquant un processus systematique et le code est derive des termes algebriques des pre- et post-conditions. Notre specification algebrico-operationnelle permet de separer en deux etapes le processus d'obtention du code. La premiere etape consiste en l'obtention de la specification algebrico-operationnelle a partir des specifications algebriques des types abstraits. La deuxieme etape a trait a l'implementation en partant des specifications operationnelles obtenue dans la phase precedente. Nous cherchons a produire des programmes imperatifs, c'est-a-dire, des programmes dont le code est exprime dans des langages de programmation de type imperatif. Le point crucial dans ce processus est l'introduction des caracteristiques des programmes imperatifs, telles que la suite d'instructions, l'affectation, les appels de fonctions et de procedures, etc. , ceci en partant des termes algebriques exprimees dans le style fonctionnel. Une des originalites de notre methode est de conduire a la production de code imperatif, et non seulement fonctionnel, ainsi que la facon de produire le code. Notre methode de developpement de logiciel etablit donc un lien effectif entre les specifications et les programmes imperatifs