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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Arlt, S., Rümmer, P., Schäf, M.: Joogie: from Java through Jimple to Boogie. In: SOAP@PLDI, pp. 3–8. ACM (2013)
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
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
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
Hickey, R.: The Clojure programming language. In: Proceedings of the 2008 Symposium on Dynamic Languages, DLS 2008, p. 1:1. ACM, New York (2008)
Rustan, K., Leino, M.: This is Boogie 2 (2008)
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
Meyer, B.: Applying “design by contract”. Computer 25(10), 40–51 (1992)
Hickey, R., Mometto, N.: clojure.tools.analyzer - analyzer for clojure code (2013). https://github.com/clojure/tools.analyzer
Pinzaru, G.: Speculator (2019). https://github.com/Ferossgp/speculator
Reznikova, S., Rivera, V., Lee, J., Mazzara, M.: Translation from event-B into Eiffel. MAIS 25(6), 623–636 (2018)
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
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)
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)
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
Rivera, V., Meyer, B.: Autoframe: automatic frame inference for object-oriented languages. Under submission (2019). https://arxiv.org/pdf/1808.08751.pdf
Rohner, A.: Spectrum (2019). https://github.com/arohner/spectrum
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
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
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)