En informática e ingeniería de software , Alloy es un lenguaje de especificación declarativa para expresar restricciones estructurales complejas y comportamiento en un sistema de software . Alloy proporciona una herramienta de modelado estructural simple basada en lógica de primer orden . [1] Alloy está destinado a la creación de micromodelos cuya corrección se puede comprobar automáticamente . Las especificaciones de la aleación se pueden verificar utilizando el analizador de aleación.
Aunque Alloy está diseñado teniendo en mente el análisis automático, Alloy se diferencia de muchos lenguajes de especificación diseñados para la verificación de modelos en que permite la definición de infinitos modelos. El analizador de aleación está diseñado para realizar comprobaciones de alcance finito incluso en modelos infinitos.
El lenguaje y el analizador Alloy son desarrollados por un equipo dirigido por Daniel Jackson en el Instituto Tecnológico de Massachusetts en Estados Unidos .
La primera versión del lenguaje Alloy apareció en 1997. Era un lenguaje de modelado de objetos bastante limitado . Las iteraciones sucesivas del lenguaje "añadieron cuantificadores , relaciones de aridad superiores , polimorfismo , subtipos y firmas". [2]
Los fundamentos matemáticos del lenguaje estuvieron fuertemente influenciados por la notación Z , y la sintaxis de Alloy le debe más a lenguajes como Object Constraint Language .
El Alloy Analyzer fue desarrollado específicamente para admitir los llamados "métodos formales livianos". Como tal, su objetivo es proporcionar un análisis totalmente automatizado, en contraste con las técnicas interactivas de demostración de teoremas comúnmente utilizadas con lenguajes de especificación similares a Alloy. El desarrollo del analizador se inspiró originalmente en el análisis automatizado proporcionado por los verificadores de modelos . Sin embargo, la verificación de modelos no se adapta al tipo de modelos que normalmente se desarrollan en Alloy y, como resultado, el núcleo del analizador finalmente se implementó como un buscador de modelos construido sobre un solucionador SAT booleano . [1]
Hasta la versión 3.0, el Alloy Analyzer incorporó un buscador de modelos integral basado en SAT basado en un solucionador SAT disponible en el mercado. Sin embargo, a partir de la versión 4.0, el Analizador utiliza el buscador de modelos Kodkod, para el cual el Analizador actúa como interfaz. Ambos buscadores de modelos esencialmente traducen un modelo expresado en lógica relacional a una fórmula lógica booleana correspondiente y luego invocan un solucionador SAT disponible en el mercado para la fórmula booleana. En el caso de que el solucionador encuentre una solución, el resultado se traduce nuevamente en la correspondiente vinculación de constantes a variables en el modelo de lógica relacional. [3]
Para garantizar que el problema de búsqueda de modelos sea decidible , Alloy Analyzer realiza la búsqueda de modelos en ámbitos restringidos que consisten en un número finito de objetos definido por el usuario. Esto tiene el efecto de limitar la generalidad de los resultados producidos por el analizador. Sin embargo, los diseñadores del Alloy Analyzer justifican la decisión de trabajar dentro de alcances limitados apelando a la hipótesis de alcance pequeño : que se puede encontrar una alta proporción de errores probando un programa para todas las entradas de prueba dentro de un alcance pequeño. [4]
Los modelos de aleación son de naturaleza relacional y se componen de varios tipos diferentes de declaraciones: [1]
sig Object{}define un objeto de firmasig List{ head : lone Node }define una Lista de firma que contiene un encabezado de campo de tipo Nodo y multiplicidad sola : esto establece la existencia de una relación entre Listas y Nodos de modo que cada Lista esté asociada con no más de un Nodo principalDebido a que Alloy es un lenguaje declarativo, el significado de un modelo no se ve afectado por el orden de las declaraciones.