Transformations certifiées de programmes impératifs

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.
Type de document :
Rapport
[Research Report] rapport CEDRIC No 398, 2002, pp.15
Liste complète des métadonnées

Littérature citée [4 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00165957
Contributeur : Sandrine Blazy <>
Soumis le : lundi 30 juillet 2007 - 15:50:47
Dernière modification le : mardi 10 juillet 2018 - 17:02:03
Document(s) archivé(s) le : lundi 24 septembre 2012 - 11:26:02

Fichier

article_cedric.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00165957, version 1

Collections

Citation

Sandrine Blazy. Transformations certifiées de programmes impératifs. [Research Report] rapport CEDRIC No 398, 2002, pp.15. 〈inria-00165957〉

Partager

Métriques

Consultations de la notice

132

Téléchargements de fichiers

61