Towards Static Verification of Clojure Contract-Based Programs

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.