Abstract FR:

Le but de cette thèse est de présenter un nouveau formalisme de traitement d'exceptions dans le cadre des types abstraits algébriques, et de l'utiliser pour traiter l'implémentation abstraite en présence d'exceptions. La première partie développe une nouvelle sémantique pour l'implémentation abstraite, et permet d'exprimer la correction d'une implémentation en terme de suffisante complétude et consistance hiérarchique. Ainsi les preuves de correction d'une implémentation abstraite peuvent être traitées par des méthodes classiques telles que les techniques de réécriture ou d'induction structurelle. L'idée majeure de cette approche repose sur une distinction fondamentale entre spécifications descriptives et spécifications constructives. Des conditions simples et peu restrictives sont fournies pour que la composition d'implémentations correctes reste correcte. La seconde partie développe un nouveau formalisme de traitement d'exceptions : les exception-algèbres. Ce formalisme autorise toutes les formes de traitement d'exceptions (messages d'erreur, propagation implicite des exceptions et des erreurs, récupérations d'exceptions), tout en préservant l'existence des modèles initiaux et une approche fonctorielle simple. Nous définissons en particulier une sémantique fonctorielle des enrichissements, munie des notions de consistance hiérarchique et de suffisante complétude. Pius généralement, la plupart des primitives de structuration des spécifications algébriques peuvent être étendues sans difficulté aux exception-algèbres car les résultats fondamentaux relatifs aux exception-algèbres sont analogues à celles des types abstraits algébriques "classiques". La troisième partie démontre en particulier que le formalisme d'implémentation abstraite peut être étendu aux exception-algèbres sans difficulté. Plusieurs exemples d’exception-spécifications et d'implémentations abstraites sont donnés en annexe.