Skip to Main content Skip to Navigation
Conference papers

A Modular Way to Reason About Iteration

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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [16 references]  Display  Hide  Download

https://hal.inria.fr/hal-01281759
Contributor : Mário José Parreira Pereira <>
Submitted on : Monday, May 9, 2016 - 11:28:29 AM
Last modification on : Tuesday, April 21, 2020 - 1:03:56 AM
Document(s) archivé(s) le : Tuesday, November 15, 2016 - 10:36:17 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

532

Files downloads

1303