Automatic test-case generation for Haskell based on dependent types

Abstract

Software testing is the simplest and most widespread approach to finding bugs in computer programs, where bugs are understood as a discrepancy between the expected output of the program and its actual output. Testing has the disadvantage of requiring a previous generation of a suite of test cases—inputs to the program that are representative of the whole input space—together with the expected outputs. Property-based testing addresses this issue by requiring only a formal specification of the intended behavior of the code and generating test cases automatically: then, the functional correctness of the program can be tested empirically by checking if the output of the program when given the generated test cases as input satisfies the specification.

A naïve implementation of property-based testing behaves poorly when the tested program has non-trivial preconditions: these are usually written in the specification as a conditional statement of the form “if the input meets some condition, then the output should satisfy some other condition”, but values generated at random frequently do not satisfy the precondition, meaning that the specification holds vacuously—a false premise makes any implication true, regardless of the conclusion.

Our work aims to solve the above problem by using a dependent type system to encode the desired preconditions at the type level. We start by developing a mechanism to automatically construct test case generators from data type declarations. Then, we show how dependent types can be simulated in Haskell using advanced features such as GADTs and data type promotion, and finally we extend our mechanism to translate (simulated) dependent type declarations into test case generators that only produce values satisfying the specified precondition.El testing es el método más sencillo y extendido para encontrar errores en programas de ordenador, entendiendo un error como una discrepancia entre la salida que se espera del programa y la salida que realmente produce éste. No obstante, el testing tiene el inconveniente de que requiere haber producido previamente una serie de casos de prueba—valores de entrada al programa que sean representativos de todo el espacio de posibles entradas—así como las salidas esperadas. El testing basado en propiedades (property-based testing o PBT, en inglés) aborda este problema requiriendo únicamente una especificación formal del comportamiento esperado del programa, y generando los casos de prueba de manera automática: así, la corrección funcional del programa se verifica empíricamente comprobando si la salida que produce programa al recibir como entrada los valores generados satisface o no la especificación

Una implementación ingenua de PBT puede dar malos resultado cuando el programa analizado tiene precondiciones no triviales: éstas normalmente se codifican en la especificación como un enunciado condicional de la forma “si la entrada satisface alguna condición, entonces la salida debería satisfacer alguna otra condición”, pero es común que los valores generados al azar no cumplan la precondición, haciendo que la especificación se verifique de manera trivial, ya que una premisa falsa hace cierta cualquier implicación, sin importar cuál sea la conclusión.

Este trabajo pretende resolver el problema descrito usando un sistema de tipos dependientes para codificar las precondiciones. En primer lugar, desarrollamos un mecanismo para construir automáticamente generadores de casos de prueba a partir de declaraciones de tipos de datos. A continuación, mostramos cómo se puede simular un sistema de tipos dependientes en Haskell usando características avanzadas como GADTs o promoción de tipos de datos, y finalmente extendemos el mecanismo de traducción para transformar es- tas declaraciones de tipos dependientes simulados en generadores de casos de prueba que solo produzcan valores que satisfagan la precondición establecida.