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

Abstract

When it comes to software development, programmers find themselves hardly implement- ing anything from scratch, relying on internal or third-party libraries with pre-written code. Besides providing genericity, abstraction, and performant features, by encapsulat- ing everything in a library, we are more keen to standardize code that has been formally proved correct. This work aims to formally prove a subset of the OCamlGraph library, with special concern on algorithms that employ higher-order iteration. By asserting the correctness of its algorithms, its users can feel safer knowing that the library is not error-inducing. We will base ourselves on GOSPEL specifications that can be consumed by the verification framework Cameleer. As most graph algorithms in the OCamlGraph library employ some sort of higher-ordered iteration, we seek to answer the question: “How to soundly and reliably formally verify implementations and clients of OCaml higher-order iteration, using mostly automated proof tools?”. In this document, we outline some theoretical and practical background concerning deductive verification in the functional paradigm and available techniques for specifying and verifying higher-order iteration. We also present our methodology for the specifica- tion and verification of higher-order iterators in OCaml using GOSPEL specifications. We complement this methodology with a collection of case studies that sustain our work.

No que toca ao desenvolvimento de software, os programadores raramente implementam muita coisa de raiz, dando uso a bibliotecas, quer internas ou de terceiros, com código pré-escrito. Para além da genericidade, da abstracção, e de componentes com um alto desempenho que costumam oferecer, a encapsulação de código numa biblioteca permite a sua normalização, se este for provado correto. Este trabalho propõe verificar formalmente um subconjunto da biblioteca OCamlGraph, com especial interesse em algoritmos que empreguem iteração de ordem superior. Ao afirmarmos a correção dos seus algoritmos, os seus utilizadores podem sentir-se mais confiantes ao saber que, pelo menos, a biblioteca não induzirá em erros. O trabalho vai ser baseado em especificações na linguagem GOSPEL que, por sua vez, serão consumidas pela plataforma de verificação Cameleer. A observação de que grande parte dos algoritmos da biblioteca OCamlGraph utiliza iteração de ordem superior, leva-nos a procurar responder à questão: “Como verificar formalmente, de modo completo e fiável, implementações e o consumo da iteração de ordem superior em OCaml, recorrendo a ferramentas de prova automática?”. Neste documento, vamos abordar algum fundamento teórico e prático no que diz respeito a verificação dedutiva no paradigma de programação funcional e algumas técnicas para especificação e verificação de iteração de ordem superior. Apresentamos ainda a nossa metodologia para a especificação e verificação destes mesmos iteradores, em OCaml, com o uso de especificaçãos na linguagem GOSPEL. Complementamos a nossa metodologia com uma coleção de casos de estudos que sustêm o nosso trabalho.