Verificación automática de programes basada en semántica de comportament i lógica de primer ordreel método Alice

Resumen

Se presenta un método de verificación automática llamado Alice (algebraic inference of the correctness of environments), dado un programa P y una especificación algebraica SP1, Alice determina si P es correcto respecto a SP1. Para hacer esto, Alice construye primero una especificación algebraica SP2 que es equivalente (es decir, tiene la misma semántica) a P. Así, determinar la corrección de P respecto a SP1 se reduce a comprobar la equivalencia de dos especificaciones SP1 y SP2, según una nueva noción de equivalencia definida en la tesis. A partir de SP1 y SP2, Alice construye una especificación SP3 y un conjunto I de teoremas inductivos de forma que demostrar la equivalencia de SP1 y SP2 se reduce a demostrar I en el álgebra inicial de SP3. De esta forma, Alice determina la corrección de P respecto a SP1 comprobando (con un demostrador de teoremas inductivos) la satisfacción de I en el álgebra inicial de SP3. La principal novedad del método Alice es que la verificación es totalmente automática y que, en lugar de trabajar comparando un programa y su especificación, se hacen las transformaciones adecuadas para trabajar con dos especificaciones (que son objetos similares) y este hecho facilita notablemente el proceso Alice no es un procedimiento de decisión (ya que el problema es indecidible) y se puede extender para tratar otros problemas, como el de la equivalencia entre módulos.