Skip to main content
SpringerLink
Log in

Towards Static Verification of Clojure Contract-Based Programs

  • Conference paper
  • First Online:
Software Technology: Methods and Tools (TOOLS 2019)

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

Included in the following conference series:

Abstract

Detecting possible weaknesses in a dynamically typed functional programming language at compile time plays an important role in the development of correct Software. Unfortunately, this is still an open problem for some functional programming languages. This paper proposes a translation of Clojure programs into Boogie. Thus, users can write formal specifications of Clojure programs, using pre- and postconditions that are supported by the language, translate the code to Boogie, and use Boogie’s automated theorem provers to formally check the correctness of the code w.r.t. its specifications. This enables users to formally prove Clojure programs enriched with pre- and post-conditions. This paper shows the translation rules, its implementation and discusses some of the challenges faced due to differences between the source and the target languages.

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

References

  1. Arlt, S., Rümmer, P., Schäf, M.: Joogie: from Java through Jimple to Boogie. In: SOAP@PLDI, pp. 3–8. ACM (2013)

    Google Scholar 

  2. Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: an overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-30569-9_3

    Chapter  Google Scholar 

  3. Cataño, N., Rivera, V.: EventB2Java: a code generator for event-B. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 166–171. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40648-0_13

    Chapter  Google Scholar 

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

  5. Hickey, R.: The Clojure programming language. In: Proceedings of the 2008 Symposium on Dynamic Languages, DLS 2008, p. 1:1. ACM, New York (2008)

    Google Scholar 

  6. Rustan, K., Leino, M.: This is Boogie 2 (2008)

    Google Scholar 

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

  8. Meyer, B.: Applying “design by contract”. Computer 25(10), 40–51 (1992)

    Article  Google Scholar 

  9. Hickey, R., Mometto, N.: clojure.tools.analyzer - analyzer for clojure code (2013). https://github.com/clojure/tools.analyzer

  10. Pinzaru, G.: Speculator (2019). https://github.com/Ferossgp/speculator

  11. Reznikova, S., Rivera, V., Lee, J., Mazzara, M.: Translation from event-B into Eiffel. MAIS 25(6), 623–636 (2018)

    Google Scholar 

  12. Rivera, V., Bhattacharya, S., Cataño, N.: Undertaking the tokeneer challenge in event-B. In 2016 IEEE/ACM 4th FME Workshop on Formal Methods in Software Engineering (FormaliSE), pp. 8–14, May 2016

    Google Scholar 

  13. Rivera, V., Cataño, N.: Translating event-B to JML-specified java programs. In: Proceedings of the 29th Annual ACM Symposium on Applied Computing, SAC 2014, pp. 1264–1271. ACM, New York (2014)

    Google Scholar 

  14. Rivera, V., Cataño, N., Wahls, T., Rueda, C.: Code generation for event-B. Int. J. Softw. Tools Technol. Transf. 19(1), 31–52 (2017)

    Article  Google Scholar 

  15. Rivera, V., Lee, J.Y., Mazzara, M.: Mapping event-B machines into Eiffel programming language. In: Ciancarini, P., Mazzara, M., Messina, A., Sillitti, A., Succi, G. (eds.) SEDA 2018. AISC, vol. 925, pp. 255–264. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-14687-0_23

    Chapter  Google Scholar 

  16. Rivera, V., Meyer, B.: Autoframe: automatic frame inference for object-oriented languages. Under submission (2019). https://arxiv.org/pdf/1808.08751.pdf

  17. Rohner, A.: Spectrum (2019). https://github.com/arohner/spectrum

  18. Tschannen, J., Furia, C.A., Nordio, M., Polikarpova, N.: AutoProof: auto-active functional verification of object-oriented programs. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 566–580. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_53

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Innopolis University, Innopolis, Russia

    Gheorghe Pinzaru & Victor Rivera

Authors
  1. Gheorghe Pinzaru
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Victor Rivera
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Victor Rivera .

Editor information

Editors and Affiliations

  1. Innopolis University, Innopolis, Russia

    Manuel Mazzara

  2. IUT de Blagnac , Blagnac, France

    Jean-Michel Bruel

  3. Innopolis University, Innopolis, Russia

    Bertrand Meyer

  4. Ivannikov Institute for System Programming, Russian Academy of Sciences, Moscow, Russia

    Alexander Petrenko

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

Pinzaru, G., Rivera, V. (2019). Towards Static Verification of Clojure Contract-Based Programs. In: Mazzara, M., Bruel, JM., Meyer, B., Petrenko, A. (eds) Software Technology: Methods and Tools. TOOLS 2019. Lecture Notes in Computer Science(), vol 11771. Springer, Cham. https://doi.org/10.1007/978-3-030-29852-4_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-29852-4_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-29851-7

  • Online ISBN: 978-3-030-29852-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation