En informática e ingeniería de software , Alloy es un lenguaje de especificación declarativo para expresar comportamientos y restricciones estructurales complejos en un sistema de software . Alloy proporciona una herramienta de modelado estructural simple basada en lógica de primer orden . [1] Alloy está orientado a la creación de micromodelos que luego se pueden verificar automáticamente para comprobar su corrección . Las especificaciones de Alloy se pueden verificar utilizando Alloy Analyzer.
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 modelos infinitos. Alloy Analyzer está diseñado para realizar verificaciones de alcance finito incluso en modelos infinitos.
El lenguaje y el analizador Alloy fueron 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 posteriores del lenguaje "añadieron cuantificadores , relaciones de aridad más altas , polimorfismo , subtipificación y firmas". [2]
Los fundamentos matemáticos del lenguaje estuvieron fuertemente influenciados por la notación Z , y la sintaxis de Alloy debe más a lenguajes como Object Constraint Language .
El analizador Alloy fue desarrollado específicamente para soportar los llamados "métodos formales ligeros". Como tal, está destinado a proporcionar un análisis completamente automatizado, en contraste con las técnicas de demostración de teoremas interactivas que se utilizan comúnmente 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 es adecuada para el tipo de modelos que se desarrollan típicamente 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]
A partir de la versión 3.0, Alloy Analyzer incorporó un buscador de modelos basado en SAT integrado que se basa en un solucionador SAT estándar. Sin embargo, a partir de la versión 4.0, el analizador utiliza el buscador de modelos Kodkod, para el cual actúa como interfaz. Ambos buscadores de modelos traducen esencialmente un modelo expresado en lógica relacional en una fórmula lógica booleana correspondiente y luego invocan un solucionador SAT estándar en la fórmula booleana. En caso de que el solucionador encuentre una solución, el resultado se traduce nuevamente en una vinculación correspondiente 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 definidos por el usuario. Esto tiene el efecto de limitar la generalidad de los resultados producidos por el analizador. Sin embargo, los diseñadores de Alloy Analyzer justifican la decisión de trabajar dentro de ámbitos limitados mediante una apelación a la hipótesis de ámbito pequeño : que se puede encontrar una alta proporción de errores probando un programa para todas las entradas de prueba dentro de un ámbito 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 firmas que contiene un campo de cabecera de tipo Nodo y multiplicidad única - esto establece la existencia de una relación entre Listas y Nodos de manera que cada Lista esté asociada con no más de un Nodo de cabeceraDado que Alloy es un lenguaje declarativo, el significado de un modelo no se ve afectado por el orden de las declaraciones.