Skip to Main content Skip to Navigation
New interface
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 metadata

Cited literature [16 references]  Display  Hide  Download
Contributor : Mário José Parreira Pereira Connect in order to contact the contributor
Submitted on : Monday, May 9, 2016 - 11:28:29 AM
Last modification on : Saturday, June 25, 2022 - 10:20:32 PM
Long-term archiving on: : Tuesday, November 15, 2016 - 10:36:17 PM


Files produced by the author(s)


  • HAL Id : hal-01281759, version 2


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⟩



Record views


Files downloads