Resumen de COMPAS: un compilador para un lenguaje imperativo con aserciones embebidas
en este artículo se presenta un compilador para un lenguaje de programación imperativo con aserciones embebidas. El código generado por el compilador comprueba, en tiempo de ejecución, si las aserciones son satisfechas por los datos correspondientes a dicha ejecución. Como lenguaje de especificación se usa la Lógica de Primer Orden. El lenguaje de especificación dispone, además de aserciones genéricas, de elementos especializados: aserciones Pre/Post para la especificación de procedimientos y funciones y aserciones de invarianza y expresiones de cota para bucles. Dado que uno de los objetivos buscados era que la herramienta fuera utilizable en diferentes plataformas, el compilador ha sido desarrollado en Java, y el código generado son bytecodes de Java.
