Cooq :plug-in de Coq para Eclipse

Abstract

El objetivo principal de este proyecto es la obtención de una herramienta que oficie de entorno de desarrollo para el asistente de pruebas Coq y que a su vez sea integrable con algún entorno pre existente. Se optó por usar Eclipse como entorno huésped debido a su arquitectura fácilmente extensible y su gran popularidad entre los miembros de la comunidad de desarrolladores de software. Estas propiedades son causales del gran número de plugins que existen para este entorno de desarrollo. Esto, sin lugar a dudas, suma otro punto a favor para su elección, ya que abre las puertas a la integración de esta nueva herramienta con una gran gama de plugins para Eclipse. Para el desarrollo de esta nueva herramienta fue necesario relevar todas aquellas herramientas que cumplieran, en algún sentido, con las necesidades planteadas, con el objetivo de conocer la oferta existente y así poder confeccionar la lista de requerimientos que debería implementar la herramienta, que hemos dado a llamar Coop. Coop no es solo una acumulación de funcionalidades soportadas por otras herramientas, sino que incorpora varias funcionalidades innovadoras como resultado de sugerencias realizadas por usuarios expertos en el uso de Coq. Entre estas funcionalidades se encuentra la ejecución independientemente de bloques específicos de código, la construcción de un árbol de derivación a medida que avanza una prueba y su exportación a diferentes formatos, la generación de un grafo de dependencias del código, la posibilidad de navegar a través del código en base a palabras clave, entre otras. Estas funcionalidades hacen de Coop un entorno innovador de desarrollo para Coq en Eclipse, amigable y con gran poder de asistencia al usuario en pro de facilitar el uso de Coq.