A Modular Way to Reason About Iteration

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
Abstract : In this paper we present an approach to specify programs performing iterations. The idea is to specify iteration in terms of the nite sequence of the elements enumerated so far, and only those. In particular, we are able to deal with non-deterministic and possibly innite iteration. We show how to cope with the issue of an iteration no longer being consistent with mutable data. We validate our proposal using the deductive verication tool Why3 and two iteration paradigms, namely cursors and higher-order iterators. For each paradigm, we verify several implementations of iterators and client code. This is done in a modular way, i.e., the client code only relies on the specication of the iteration.
Type de document :
Communication dans un congrès
8th NASA Formal Methods Symposium, Jun 2016, Minneapolis, United States
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01281759
Contributeur : Mário José Parreira Pereira <>
Soumis le : lundi 9 mai 2016 - 11:28:29
Dernière modification le : jeudi 5 avril 2018 - 12:30:22
Document(s) archivé(s) le : mardi 15 novembre 2016 - 22:36:17

Fichier

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

Identifiants

  • HAL Id : hal-01281759, version 2

Citation

Jean-Christophe Filliâtre, Mário Pereira. A Modular Way to Reason About Iteration. 8th NASA Formal Methods Symposium, Jun 2016, Minneapolis, United States. 〈hal-01281759v2〉

Partager

Métriques

Consultations de la notice

391

Téléchargements de fichiers

458