Le chameau et le serpent rentrent dans un bar : vérification quasi-automatique de code OCaml en logique de séparation
Charlène Gros, Mário Pereira
TL;DR
Le document décrit une extension de Cameleer, gospel2viper, qui traduit des programmes OCaml annotés avec Gospel vers l’intermédiaire $Viper$ fondé sur la logique de séparation afin de vérifier automatiquement des programmes manipulant le tas. En dépassant les limitations du backend Why3 pour les structures mutables récursives, l’approche encode les types algébriques via des ADTs et introduit des notions de possession de champs ($acc$ et $\leadsto$) ainsi que les opérations $fold$/$unfold$ pour gérer les prédicats de représentation. L’article détaille l’encodage des listes et d’un module OCaml Queue, illustrant une preuve quasi-automatique des opérations d’une file (création, ajout et concatenation) via des lemmas et des prédicats comme $cellSeg$ et $Queue$. Cette approche accroît la portée de la vérification déductive des programmes OCaml en autorisant des structures allouées dynamiquement et ouvre des perspectives d’étendre le back-end à d’autres structures et d’automatiser davantage les étapes de folding et unfolding, ce qui peut impacter positivement l’assurance de correctness des programmes heap-allocated en OCaml.
Abstract
This paper presents a translation from Gospel-annotated OCaml programs into Viper, an intermediate verification language featuring Separation Logic. The practical goal is to extend Cameleer with a new back-end to prove heap-dependent OCaml programs. The logical specification of such OCaml programs is described using an extension of Gospel to support Separation Logic features, which we describe in the paper.