A Modular Way to Reason About Iteration - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2016

A Modular Way to Reason About Iteration

Résumé

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.
Fichier principal
Vignette du fichier
main.pdf (417.25 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01281759 , version 1 (02-03-2016)
hal-01281759 , version 2 (09-05-2016)

Identifiants

  • HAL Id : hal-01281759 , version 2

Citer

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⟩
485 Consultations
845 Téléchargements

Partager

Gmail Facebook X LinkedIn More