TY - GEN
T1 - A modular way to reason about iteration
AU - Filliâtre, Jean Christophe
AU - Pereira, Màrio
N1 - Publisher Copyright:
© Springer International Publishing Switzerland 2016.
PY - 2016/1/1
Y1 - 2016/1/1
N2 - In this paper we present an approach to specify programs performing iterations. The idea is to specify iteration in terms of the finite sequence of the elements enumerated so far, and only those. In particular, we are able to deal with non-deterministic and possibly infinite 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 verification 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 specification of the iteration.
AB - In this paper we present an approach to specify programs performing iterations. The idea is to specify iteration in terms of the finite sequence of the elements enumerated so far, and only those. In particular, we are able to deal with non-deterministic and possibly infinite 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 verification 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 specification of the iteration.
U2 - 10.1007/978-3-319-40648-0_24
DO - 10.1007/978-3-319-40648-0_24
M3 - Conference contribution
AN - SCOPUS:84976641053
SN - 9783319406473
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 322
EP - 336
BT - NASA Formal Methods - 8th International Symposium, NFM 2016, Proceedings
A2 - Tkachuk, Oksana
A2 - Rayadurgam, Sanjai
PB - Springer Verlag
T2 - 8th International Symposium on NASA Formal Methods, NFM 2016
Y2 - 7 June 2016 through 9 June 2016
ER -