Abstract FR:

Nous proposons dans le cadre de cette thèse, un système qui permet de transformer un programme en une spécification équivalente. Nous supposons que le programme à transformer est récursif et qu'il se présente sous forme d'un ensemble de règles. Chaque règle du programme représente un cas particulier de décomposition des données du programme et représente donc un fragment de programme. Un programme peut faire appel à des sous-programmes. Le but de la méthode est de trouver la spécification formelle du problème résolu par le programme. Il s'agit alors de procéder à l'analyse du programme, règle par règle, pour essayer de généraliser l'ensemble des règles définissant le programme. Cette généralisation qui doit représenter la spécification recherchée est faite à l'aide d'une base de connaissances définissant la spécification complète du domaine des données du programme. La base de connaissances est donnée sous forme d'un système de réécriture complet comprenant les différentes définitions d'opérateurs liées aux types de données utilisés par le programme grâce à la définition de leurs types abstraits correspondants. La spécification ainsi obtenue est définie par une conjonction de prédicats et exprime ainsi les relations entre les variables du programme. Elle permet de comprendre de façon claire et précise ce que fait le programme.