Resumen:
In the context of the multilanguage verification platform CAVI-ART, we have defined an Intermediate Representation (IR) to which all the source languages are translated. This IR contains both the code and the assertions given by the programmer. Its primary purpose was automatically generating and proving, in a source language independent way, the verification conditions ensuring the program correctness. The logical formulas are sent by the platform to an SMT solver which checks their validity.
In this paper we present a new use of the IR: we transform it into an executable language (that it turns out to be Haskell) and also transform the assertions into executable (Haskell) code. Thanks to that, tests can be run on the transformed program, and bugs can be detected either in the specification assertions or in the code. Moreover, we use the assertions to generate black-box test-cases from them, and also as test oracles. In this way, given the IR of a program, all the process —namely, test-case generation, test running, and test correctness checking— is completely automatic. So, thousands of tests can be run with little or none effort. The only burden for the programmer is providing the precondition and the postcondition of the code under test, which anyway should have been provided in advance, since the primary goal was to verify the program.
We discuss the problems we have encountered while implementing this idea, and how we have solved them. In particular, we report on the use of Haskell resources such as GADTs, efficient data structures, and specialized libraries.