Abstract FR:

Les travaux presentes dans cette these ont pour principal objectif le developpement d'un environnement d'aide a l'utilisation d'une methode deductive de validation de programmes : le langage deva. Cet environnement, baptise devaur, et construit a partir de l'outil centaur, vise a faciliter la redaction de preuves dans le langage deva selon trois axes differents. La premiere idee est de recourir a un outil de validation automatique externe, en l'occurrence nqthm de boyer et moore, pour decharger l'utilisateur de certaines parties de preuves dont la production est ainsi rendue automatique ; cependant, l'acceptation de chaque theoreme ainsi demontre pose le probleme crucial de son bien fonde dans deva, puisque il y est introduit comme un axiome. La validite du mecanisme a ete demontree pour la logique des propositions et l'arithmetique. La formalisation de certaines proprietes mathematiques dans un langage tel que deva est bien souvent accompagnee d'une perte de semantique a l'origine d'ambiguites lors de leur application. Devaur incorpore un langage permettant aux formalisateurs de theories de fournir cette information manquante, rendant ainsi leur application deterministe. Enfin, l'interprete du langage deva utilise retourne chaque terme sous une forme delta-expansee et beta-reduite ; cette representation des termes rend leur lecture souvent ardue. Devaur propose un mecanisme permettant de delta-contracter les termes, puis de permettre l'expansion et la contraction de chaque definition inclue dans le terme, par simple designation par l'intermediaire de la souris. Afin d'evaluer les apports de devaur, nous avons ensuite formalise unity dans le langage deva, obtenant ainsi un outil relativement performant pour la validation de programmes paralleles.