|
 
|
[BUR00] Traitement des expressions dépourvues de sens de la théorie des ensembles: Application à la méthode B
Mémoire de Thèse : Soutenue le: 01 January 2000, : Traitement des expressions dépourvues de sens de la théorie des ensembles: Application à la méthode B,
motcle:
Résumé:
Ce travail porte sur la définition d'une logique pour un langage avecfonctions partielles. Une interprétation tri-valuée est choisiepour les formules. A partir de cette sémantique, une relation deconséquence est définie et deux systèmes de déduction incorporant lespreuves de bonne definition sont proposés, le dernier a l'avantagede ne pas melanger les preuves de bonne définition avec les preuvesusuelles et donne ainsi à l'utilisateur l'impression de toujourstravailler dans une logique à deux valeurs. Ces choix ont été guidespar le fait que ce système a pour objectif d'ètre implanté dans unoutil d'aide à la preuve. Ce travail a ete etendu sur un langage avec fonction partielle quiest le langage logique sous jacent à la méthode B. Un outil de generation d'obligations de preuve de bonne definition estspécifie. Ces preuves sont ajoutées aux preuves de validation desdifférents composants B.
BibTeX
| @phdthesis { | |||
| BUR00, | |||
| title | = | "{Traitement des expressions dépourvues de sens de la théorie des ensembles: Application à la méthode B}", | |
| author | = | "L. Burdy", | |
| year | = | 2000, | |
| address | = | "{CEDRIC Laboratory, Paris, France}", | |
| } |
