|
 
|
[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:
sys
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", | |
| } | |||
