Abstract
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.
This research was partly supported by the French National Research Organization (project VOCAL ANR-15-CE25-008).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
The triples are obtained by applying our translation scheme; more concise triples may be derived for \ofpush and \ofcreate by eliminating existential quantifiers.
- 2.
We patched the parser from the OCaml compiler so as to process comments of the form (*@ ...*) as if they were written as OCaml attributes of the form [@@gospel “...”]. The OCaml parser already processes documentation comments in this way.
- 3.
More details about the Why3 workflow may be found in Pereira’s PhD thesis [30].
- 4.
References
Baudin, P., Filliâtre, J.C., Marché, C., Monate, B., Moy, Y.,Prevosto, V.: ACSL: ANSI/ISO C Specification Language, version 1.4 (2009). http://frama-c.cea.fr/acsl.html
Bobot, F., Conchon, S., Contejean, E., Iguernelala, M., Lescuyer, S., Mebsout, A.: The Alt-Ergo automated theorem prover (2008). http://alt-ergo.lri.fr/
Carré, B., Garnsworthy, J.: SPARK–an annotated Ada subset for safety-critical programming. In: Proceedings of the Conference on TRI-Ada 1990, New York, NY, USA, pp. 392–402. ACM Press (1990)
Cauderlier, R., Sighireanu, M.: A verified implementation of the bounded list container. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 172–189. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89960-2_10
Charguéraud, A.: Characteristic Formulae for Mechanized Program Verification. PhD thesis, Université Paris (2010). http://www.chargueraud.org/arthur/research/2010/thesis/
Charguéraud, A.: Characteristic formulae for the verification of imperative programs. In: Manuel, M.T., Chakravarty, Hu, Z., Danvy, O. (eds.) Proceeding of the 16th ACM SIGPLAN International Conference on Functional Programming (ICFP), Tokyo, Japan, pp. 418–430. ACM, September 2011
Charguéraud, A., Pottier, F.: Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits. J. Autom. Reasoning (2017)
Charguéraud, A., Pottier, F.: Temporary read-only permissions for separation logic. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 260–286. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54434-1_10
Cousot, P.,Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The ASTRÉE analyzer. In: ESOP, number 3444 in Lecture Notes in Computer Science, pp. 21–30 (2005)
Cruanes, S., Grinberg, R., Deplaix, J.-P., Midtgaard, J.: Qcheck (2019). https://github.com/c-cube/qcheck
de Gouw, S., de Boer, F.S., Bubel, R., Hähnle, R., Rot, J., Steinhöfel, D.: Verifying OpenJDK’s sort method for generic collections. J. Autom. Reasoning (2017)
Filliâtre, J.-C.: One logic to use them all. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 1–20. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38574-2_1
Filliâtre, J.-C., Paskevich, A.: Why3 — where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37036-6_8
Guéneau, A., Charguéraud, A., Pottier, F.: A fistful of dollars: formalizing asymptotic complexity claims via deductive program verification. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 533–560. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89884-1_19
Hatcliff, J., Leavens, G.T., Leino, K.R.M., Müller, P., Parkinson, M.: Behavioral interface specification languages. ACM Comput. Surv. 44(3), 16:1–16:58 (2012)
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580, 583 (1969)
Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41–55. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20398-5_4
Kassios, I.T.: Dynamic frames and automated verification (2011). Tutorial for the 2nd COST Action IC0701 Training School, Limerick 6/11, Ireland
Kassios, I.T.: The dynamic frames theory. Formal Aspects Comput. 23(3), 267–288 (2011)
Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-c: a software analysis perspective. Formal Aspects Comput. 27(3), 573–609 (2015)
Klein, G., et al.: seL4: formal verification of an OS kernel. Commun. ACM 53(6), 107–115 (2010)
Kosmatov, N., Marché, C., Moy, Y., Signoles, J.: Static versus dynamic verification in Why3, Frama-C and SPARK 2014. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 461–478. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47166-2_32
Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98–06i, Iowa State University (2000)
Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348–370. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17511-4_20
Leino, K.R.M., Müller, P.: A basis for verifying multi-threaded programs. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 378–393. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00590-9_27
Leroy, X.: A formally verified compiler back-end. J. Autom. Reasoning 43(4), 363–446 (2009)
Müller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 41–62. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49122-5_2
Mével, G., Jourdan, J.-H., Pottier, F.: Time credits and time receipts in iris. In: Caires, L. (ed.) ESOP 2019. LNCS, vol. 11423, pp. 3–29. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17184-1_1
Parkinson, M.J., Summers, A.J.: The relationship between separation logic and implicit dynamic frames. Log. Methods Comput. Sci. 8(3) (2012)
Pereira, M.J.P.: Tools and Techniques for the Verification of Modular Stateful Code. PhD thesis, Université Paris-Saclay (2018)
Polikarpova, N., Tschannen, J., Furia, C.A.: A fully verified container library. Formal Aspects Comput. 30(5), 495–523 (2018)
Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: 17th Annual IEEE Symposium on Logic in Computer Science. IEEE (2002)
Signoles, J., Kosmatov, N., Vorobyov, K.: E-ACSL, a Runtime Verification Tool for Safety and Security of C Programs (Tool Paper). In: International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CuBES 2017), September 2017
Smans, J., Jacobs, B., Piessens, F.: Implicit dynamic frames: combining dynamic frames and separation logic. In: Drossopoulou, S. (ed.) ECOOP 2009. LNCS, vol. 5653, pp. 148–172. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03013-0_8
The Coq Development Team. The Coq Proof Assistant Reference Manual - Version V8.9 (2019). http://coq.inria.fr
Acknowledgments
We are grateful to X. Leroy, F. Pottier, A. Guéneau, and A. Paskevich for discussions and comments during the preparation of this paper.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Charguéraud, A., Filliâtre, JC., Lourenço, C., Pereira, M. (2019). GOSPEL—Providing OCaml with a Formal Specification Language. In: ter Beek, M., McIver, A., Oliveira, J. (eds) Formal Methods – The Next 30 Years. FM 2019. Lecture Notes in Computer Science(), vol 11800. Springer, Cham. https://doi.org/10.1007/978-3-030-30942-8_29
Download citation
DOI: https://doi.org/10.1007/978-3-030-30942-8_29
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-30941-1
Online ISBN: 978-3-030-30942-8
eBook Packages: Computer ScienceComputer Science (R0)