Portal de Periódicos da CAPES

Towards Static Verification of Clojure Contract-Based Programs

2019; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-3-030-29852-4_5

1611-3349

Gheorghe Pinzaru, Víctor Rivera,

Distributed systems and fault tolerance

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.