GOSPEL -Providing OCaml with a Formal Specification Language

Arthur Charguéraud (1, 2) , Jean-Christophe Filliâtre (3, 4) , Cláudio Lourenço (3, 4) , Mário Pereira (5, 6)

1 CAMUS - Compilation pour les Architectures MUlti-coeurS
2 ICube - Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie
3 LRI - Laboratoire de Recherche en Informatique
4 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations
5 NOVA-LINCS - NOVA Laboratory for Computer Science and Informatics
6 FCT NOVA - Faculdade de Ciências e Tecnologia = School of Science & Technology

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 Separation 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 specifying OCaml code, we believe that many aspects of its design could apply to other programming languages. This paper presents the design and semantics of GOSPEL, and reports on its application for the development of a formally verified library of general-purpose OCaml data structures.

Domains: Logic in Computer Science [cs.LO]

Arthur Charguéraud, Jean-Christophe Filliâtre, Cláudio Lourenço, Mário Pereira. GOSPEL -Providing OCaml with a Formal Specification Language. FM 2019 : 23rd International Symposium on Formal Methods, Oct 2019, Porto, Portugal. ⟨hal-02157484v1⟩