|
|
|
Información General
|
| |
|
En esta página se encuentra la información publicada
por el Departamento de Computación.
Por cualquier solicitud, dirigirse a ivana AT dc.exa.unrc.edu.ar.
|
|
|
|
21/06/2007
|
|
Abstracción por Predicados en Especificaciones DynAlloy
|
|
Aula 102 Pab. 2. 17:30 hs
"Abstracción por Predicados en Especificaciones DynAlloy"
por N. Aguirre (trabajo conjunto con M. Frias, J.P. Galeotti, G. Regis y P. Ponzio)
DynAlloy es una extensión del lenguaje de especificaciones Alloy definida para poder describir de mejor manera el cambio de estados a través de acciones y programas, usando el estilo de la lógica dinámica. En esta charla mostraremos cómo aplicamos abstracción por predicados, que es una técnica de abstracción ampliamente conocida, para acelerar el análisis de especificaciones DynAlloy.
La aplicación de abstracción por predicados requiere la prueba de un número de condiciones de verificación, necesarias para poder construir un programa abstracto que se corresponda con el concreto sobre el cual se trabaja. El enfoque tradicional es el de utilizar un demostrador de
teoremas para realizar esta tarea. En nuestro caso, utilizaremos el Alloy Analyzer, lo cual nos lleva a una técnica completamente automática para la construcción de las abstracciones. Más aún, utilizaremos también el Alloy Analyzer para comprobar si un contraejemplo abstracto es
espúreo o no.
|
|
|
|
