Rechercher

[DR14] Verified functional iterators using the FoCaLiZe environment

Conférence Internationale avec comité de lecture : Software Engineering and Formal Methods, September 2014, pp.317--331, Series LNCS,

Mots clés: FoCaLiZe, certification, iterators, design patterns, Coq, Ocaml

Résumé: Collections and iterators are widely used in the Object community since they are standards of the Java language. We present a certified functional implementation of collections and iterators addressing the Specification And Verification of Component Based Systems 2006 challenge. More precisely we describe a FoCaLiZe implementation providing these functionalities. Our approach uses inheritance and parameterization to describe functional iterators. Our code can be run in Ocaml and is certified using Coq. We provide general specifications for collections, iterators and removable iterators together with complete implementation for collections using lists as representation and iterators over those.

Equipe: cpr

BibTeX

@inproceedings {
DR14,
title="{Verified functional iterators using the FoCaLiZe environment}",
author=" C. Dubois and R. Rioboo ",
booktitle="{Software Engineering and Formal Methods}",
year=2014,
month="September",
series="LNCS",
issue=8702,
pages="317--331",
}