Skip to Main content Skip to Navigation
Reports

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.
Document type :
Reports
Complete list of metadata

Cited literature [4 references]  Display  Hide  Download

https://hal.inria.fr/inria-00165957
Contributor : Sandrine Blazy <>
Submitted on : Monday, July 30, 2007 - 3:50:47 PM
Last modification on : Saturday, February 9, 2019 - 1:23:15 AM
Long-term archiving on: : Monday, September 24, 2012 - 11:26:02 AM

File

article_cedric.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

175

Files downloads

82