Unfolding Iterators: Specification and Verification of Higher-Order Iterators, in OCaml

TL;DR

This paper introduces a generic method for specifying and verifying higher-order iterators in OCaml, combining formal specifications with deductive verification to ensure correctness across various iteration patterns.

Contribution

It presents a novel approach that integrates Gospel specifications with the Cameleer framework for verifying higher-order iterators in OCaml, validated through multiple case studies.

Findings

Successfully verified list iterators and graph algorithms

Demonstrated the applicability of the approach to real OCaml libraries

Provided a formal foundation for reasoning about higher-order iteration

Abstract

Albeit being a central notion of every programming language, formally and modularly reasoning about iteration proves itself to be a non-trivial feat, specially in the context of higher-order iteration. In this paper, we present a generic approach to the specification and deductive verification of higher-order iterators, written in the OCaml language. Our methodology follows two key principles: first, the usage of the Gospel specification language to describe the general behaviour of any iteration schema; second, the usage of the Cameleer framework to deductively verify that every iteration client is correct with respect to its logical specification. To validate our approach we develop a set of verified case studies, ranging from classic list iterators to graph algorithms implemented in the widely used OCamlGraph library.