Sistema de validación para el desarrollo incremental de un intérprete de R en Coq

Abstract

El lenguaje de programación R es muy popular para desarrollar programas estadísticos y de análisis de datos, gracias a sus numerosas librerías y amplia comunidad, su sintaxis concisa y expresiva, así como soporte para su uso interactivo. Aún así, su semántica es bastante compleja y contiene numerosos casos de borde, y no está formalmente especificada, lo que hace difícil confiar plenamente en los programas desarrollados en R. Esto tiene como consecuencia que, en el año 2017, se inicie el proyecto CoqR, que busca formalizar la semántica de R, definiendo para ello una semántica natural en la forma de un intérprete implementado en el asistente de pruebas Coq. Como primera fuente de confianza, para validar la formalización, se utiliza una codificación monádica, que permite establecer una correspondencia visual directa entre el código en Coq y el intérprete de referencia implementado en C, GNU R, de tal forma que una o dos líneas de CoqR equivalen a una o dos de GNU R. El sistema desarrollado en esta memoria sirve como infraestructura para ejecutar bancos de pruebas y poder comparar, de manera sistemática, el comportamiento de CoqR y GNU R, proporcionando una segunda fuente de confianza para validar la formalización. Además, pro- porciona herramientas para apoyar el proceso iterativo de desarrollo, permitiendo identificar y detectar tanto las funcionalidades más relevantes a implementar, como los errores que puedan surgir durante esta fase. De esta manera, el sistema se integra directamente al proceso de desarrollo y a la validación de CoqR, logrando que, en su versión actual, cubra cerca del 30 % de los casos de pruebas, tanto de GNU R como de otro proyecto relevante, FastR.