TY - GEN
T1 - GOSPEL—providing OCaml with a formal specification language
AU - Charguéraud, Arthur
AU - Filliâtre, Jean Christophe
AU - Lourenço, Cláudio
AU - Pereira, Mário
N1 - Publisher Copyright:
© Springer Nature Switzerland AG 2019.
PY - 2019/1/1
Y1 - 2019/1/1
N2 - 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.
AB - 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.
U2 - 10.1007/978-3-030-30942-8_29
DO - 10.1007/978-3-030-30942-8_29
M3 - Conference contribution
AN - SCOPUS:85076116584
SN - 9783030309411
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 484
EP - 501
BT - Formal Methods – The Next 30 Years - 3rd World Congress, FM 2019, Proceedings
A2 - ter Beek, Maurice H.
A2 - McIver, Annabelle
A2 - Oliveira, José N.
PB - Springer
T2 - 23rd Symposium on Formal Methods, FM 2019, in the form of the 3rd World Congress on Formal Methods, 2019
Y2 - 7 October 2019 through 11 October 2019
ER -