Abstract FR:

Ce travail porte sur la définition d'une logique pour un langage avec fonctions partielles. Une interprétation tri-valuée est choisie pour les formules. A partir de cette sémantique, une relation de conséquence est définie et deux systèmes de déduction incorporant les preuves de bonne definition sont proposés, le dernier a l'avantage de ne pas melanger les preuves de bonne définition avec les preuves usuelles et donne ainsi à l'utilisateur l'impression de toujours travailler dans une logique à deux valeurs. Ces choix ont été guidespar le fait que ce système a pour objectif d'ètre implanté dans un outil d'aide à la preuve. Ce travail a été étendu sur un langage avec fonction partielle qui est le langage logique sous jacent à la méthode B. Un outil de génération d'obligations de preuve de bonne définition est spécifié. Ces preuves sont ajoutées aux preuves de validation des différents composants B.