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.