Skip to main content
SpringerLink
Log in

GOSPEL—Providing OCaml with a Formal Specification Language

  • Conference paper
  • First Online:
Formal Methods – The Next 30 Years (FM 2019)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11800))

Included in the following conference series:

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).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 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. 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. 3.

    More details about the Why3 workflow may be found in Pereira’s PhD thesis [30].

  4. 4.

    https://github.com/vocal-project/vocal.

References

  1. 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

  2. Bobot, F., Conchon, S., Contejean, E., Iguernelala, M., Lescuyer, S., Mebsout, A.: The Alt-Ergo automated theorem prover (2008). http://alt-ergo.lri.fr/

  3. 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)

    Google Scholar 

  4. 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

    Chapter  Google Scholar 

  5. Charguéraud, A.: Characteristic Formulae for Mechanized Program Verification. PhD thesis, Université Paris (2010). http://www.chargueraud.org/arthur/research/2010/thesis/

  6. 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

    Google Scholar 

  7. 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)

    Google Scholar 

  8. 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

    Chapter  Google Scholar 

  9. 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)

    Google Scholar 

  10. Cruanes, S., Grinberg, R., Deplaix, J.-P., Midtgaard, J.: Qcheck (2019). https://github.com/c-cube/qcheck

  11. 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)

    Google Scholar 

  12. 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

    Chapter  Google Scholar 

  13. 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

    Chapter  Google Scholar 

  14. 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

    Chapter  Google Scholar 

  15. 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)

    Article  Google Scholar 

  16. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580, 583 (1969)

    Article  Google Scholar 

  17. 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

    Chapter  Google Scholar 

  18. Kassios, I.T.: Dynamic frames and automated verification (2011). Tutorial for the 2nd COST Action IC0701 Training School, Limerick 6/11, Ireland

    Google Scholar 

  19. Kassios, I.T.: The dynamic frames theory. Formal Aspects Comput. 23(3), 267–288 (2011)

    Article  MathSciNet  Google Scholar 

  20. Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-c: a software analysis perspective. Formal Aspects Comput. 27(3), 573–609 (2015)

    Article  MathSciNet  Google Scholar 

  21. Klein, G., et al.: seL4: formal verification of an OS kernel. Commun. ACM 53(6), 107–115 (2010)

    Article  Google Scholar 

  22. 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

    Chapter  Google Scholar 

  23. 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)

    Google Scholar 

  24. 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

    Chapter  MATH  Google Scholar 

  25. 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

    Chapter  Google Scholar 

  26. Leroy, X.: A formally verified compiler back-end. J. Autom. Reasoning 43(4), 363–446 (2009)

    Article  MathSciNet  Google Scholar 

  27. 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

    Chapter  MATH  Google Scholar 

  28. 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

    Chapter  Google Scholar 

  29. Parkinson, M.J., Summers, A.J.: The relationship between separation logic and implicit dynamic frames. Log. Methods Comput. Sci. 8(3) (2012)

    Google Scholar 

  30. Pereira, M.J.P.: Tools and Techniques for the Verification of Modular Stateful Code. PhD thesis, Université Paris-Saclay (2018)

    Google Scholar 

  31. Polikarpova, N., Tschannen, J., Furia, C.A.: A fully verified container library. Formal Aspects Comput. 30(5), 495–523 (2018)

    Article  MathSciNet  Google Scholar 

  32. Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: 17th Annual IEEE Symposium on Logic in Computer Science. IEEE (2002)

    Google Scholar 

  33. 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

    Google Scholar 

  34. 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

    Chapter  Google Scholar 

  35. The Coq Development Team. The Coq Proof Assistant Reference Manual - Version V8.9 (2019). http://coq.inria.fr

Download references

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

  1. Inria Nancy - Grand Est, Strasbourg, France

    Arthur Charguéraud

  2. Inria Saclay - Île de France, Palaiseau, France

    Jean-Christophe Filliâtre & Cláudio Lourenço

  3. NOVA LINCS & DI, FCT, Universidade Nova de Lisboa, Lisbon, Portugal

    Mário Pereira

Authors
  1. Arthur Charguéraud
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jean-Christophe Filliâtre
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Cláudio Lourenço
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Mário Pereira
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Mário Pereira .

Editor information

Editors and Affiliations

  1. Consiglio Nazionale delle Ricerche, Pisa, Italy

    Maurice H. ter Beek

  2. Macquarie University, Sydney, NSW, Australia

    Annabelle McIver

  3. University of Minho, Braga, Portugal

    José N. Oliveira

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

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)

Publish with us

Policies and ethics

Search

Navigation