Itérer avec confiance

Jean-Christophe Filliâtre 1, 2 Mário Pereira 1, 2
2 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
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.
Type de document :
Communication dans un congrès
Journées Francophones des Langages Applicatifs, Jan 2016, Saint-Malo, France. 〈http://jfla.inria.fr/2016/〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01240891
Contributeur : Jean-Christophe Filliâtre <>
Soumis le : jeudi 10 décembre 2015 - 15:09:42
Dernière modification le : jeudi 5 avril 2018 - 12:30:22
Document(s) archivé(s) le : vendredi 11 mars 2016 - 11:54:21

Fichier

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

Identifiants

  • 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. 〈http://jfla.inria.fr/2016/〉. 〈hal-01240891〉

Partager

Métriques

Consultations de la notice

348

Téléchargements de fichiers

142