Skip to Main content Skip to Navigation
Conference papers

Itérer avec confiance

Résumé : Un curseur est une structure de données qui permet d'obtenir successivement les éléments d'une collection, tout en laissant à l'utilisateur le contrôle de cette itération. Cet article propose une spécification formelle de ce qu'est un curseur, dans le contexte de la vérification déductive, avec le double objectif de prouver que des curseurs sont correctement réalisés et correctement utilisés. En particulier, nous proposons une approche modulaire, où le code utilisant un curseur peut être prouvé sans connaître le détail d'implémentation de ce curseur. Ce travail est validé expérimentalement en utilisant l'outil Why3, au travers de nombreux exemples.
Document type :
Conference papers
Complete list of metadatas

Cited literature [14 references]  Display  Hide  Download

https://hal.inria.fr/hal-01240891
Contributor : Jean-Christophe Filliâtre <>
Submitted on : Thursday, December 10, 2015 - 3:09:42 PM
Last modification on : Tuesday, April 21, 2020 - 1:05:17 AM
Document(s) archivé(s) le : Friday, March 11, 2016 - 11:54:21 AM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01240891, version 1

Citation

Jean-Christophe Filliâtre, Mário Pereira. Itérer avec confiance. Journées Francophones des Langages Applicatifs, Jan 2016, Saint-Malo, France. ⟨hal-01240891⟩

Share

Metrics

Record views

438

Files downloads

394