GOSPEL --- Providing OCaml with a Formal Specification Language
Oct 2019
This paper introduces GOSPEL, a behavioral specification
language for OCaml. It is designed to enable modular verification of data
structures and algorithms. GOSPEL is a contract-based, strongly typed
language, with a formal semantics defined by means of translation into
Separation Logic. Compared with writing specifications directly in Sepa-
ration Logic, GOSPEL provides a high-level syntax that greatly improves
conciseness and makes it accessible to programmers with no familiarity
with Separation Logic. Although GOSPEL has been developed for speci-
fying OCaml code, we believe that many aspects of its design could apply
to other programming languages. This paper presents the design and se-
mantics of GOSPEL, and reports on its application for the development
of a formally verified library of general-purpose OCaml data structures.
Arthur Charguéraud,
Jean-Christophe Filliâtre,
Cláudio Lourenço,
Mário Pereira
