Itérer avec confiance - Archive ouverte HAL Access content directly
Conference Papers Year :

Itérer avec confiance

(1, 2) , (1, 2)
1
2

Abstract

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.
Fichier principal
Vignette du fichier
main.pdf (343.28 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01240891 , version 1 (10-12-2015)

Identifiers

  • HAL Id : hal-01240891 , version 1

Cite

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

Share

Gmail Facebook Twitter LinkedIn More