Abstract FR:

La these est composee de trois parties. La premiere partie definit de facon formelle la programmation logique par contraintes typee, enrichissement, par les types statiques, du schema classique de la programmation logique par contraintes. L'objectif de ce systeme de type prescriptif est de detecter statiquement des erreurs et d'introduir une discipline de type sur le mode de combinaison des programmes, tout en maintenant la capacite de typer les predicats de meta-programmation grace a la flexibilite du sous-typage. Un algorithme complet de verification de type est presente. L'inference de type revient a resoudre des systemes d'inegalites dont la decidabilite est connue seulement sous des hypotheses sur la structure de la relation de sous-typage. Une fois le systeme de type generique (independant de tout domaine de calcul) defini, il est applique dans la seconde partie aux structures a traits. La troisieme partie demontre de facon empirique que un systeme de programmation visuelle par contraintes peut etre construit sur le typage statique. Dans la premiere phase du processus de developpement, les types statiques, telles que les classes, et leurs semantiques, tels que leurs attributs, sont definis graphiquement. Dans la seconde phase, les associations et les contraintes sur les types statiques sont saisies de facon interactive dans le systeme. Le resultat implicite de la premiere phase est la declaration statique, tandis que le resultat de la deuxieme phase est la serie des clauses du programme qui sera execute. Une fois le probleme defini, le systeme calcule automatiquement une solution, c'est-a-dire une affectation de valeurs aux variables (attributs d'objet) telle que toutes les contraintes soient satisfaites.