|
 
|
[BLA02] Transformations certifiées de programmes impératifs
Rapport Scientifique : Date de dépot: 2002/01/01, (Tech. Rep.: CEDRIC-02-398)
motcle:
Résumé:
Nous présentons une transformation de programmes impératifs inspirée de l'évaluation partielle et
ayant été utilisée pour faciliter la compréhension d'applications scientifiques.
Ce travail a été complètement formalisé en Coq.
Partant d'une spécification du langage que nous traitons, nous avons
spécifié de façon abstraite notre analyse de code et avons prouvé sa correction sémantique.
Afin de modéliser les états-mémoire de façon abstraite, nous avons défini une couche de bas niveau
modélisant la notion générique de table d'association ainsi que des opérations sur ces tables
et contenant également des preuves de propriétés relatives aux opérations.
Nous montrons que ces tables génériques sont un exemple d'utilisation des setoïdes, ce qui
simplifie l'écriture des preuves.
BibTeX
| @techreport { | |||
| BLA02, | |||
| title | = | "{Transformations certifiées de programmes impératifs}", | |
| author | = | "S. Blazy", | |
| number | = | "{CEDRIC-02-398}", | |
| institution | = | "{CEDRIC laboratory, CNAM-Paris, France}", | |
| date | = | {01-01-2002}, | |
| } | |||
