Abstract FR:

La synthèse de programmes à partir de spécifications consiste à construire de façon systématique un algorithme à partir d’une spécification formelle. Dans notre approche, la spécification initiale et l’algorithme résultant sont exprimés sous forme de règles de réécriture, la synthèse est effectuée par une complétion partielle à la Knuth-Bendix dirigée par des stratégies. Les principales caractéristiques de notre méthode sont : - décomposition automatique d’un problème en fragments de programme (correspondant aux différentes cas de base des données). - décompositions automatique d’un problème en sous-problèmes. - correction du programme généré vis-à-vis de sa spécification.