Aleación (lenguaje de especificación)
En informática e ingeniería de software , Alloy es un lenguaje de especificación declarativa para expresar comportamientos y restricciones estructurales complejas en un sistema de software . Alloy proporciona una herramienta de modelado estructural simple basada en lógica de primer orden . [1] Alloy tiene como objetivo la creación de micro-modelos que luego se pueden verificar automáticamente para verificar su exactitud . Las especificaciones de las aleaciones se pueden verificar usando el Analizador de aleaciones.
Aunque Alloy está diseñado teniendo en cuenta 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. El analizador de aleaciones está diseñado para realizar comprobaciones de alcance finito incluso en modelos infinitos.
El analizador y el lenguaje de Alloy son desarrollados por un equipo dirigido por Daniel Jackson en el Instituto de Tecnología de Massachusetts en los Estados Unidos .
La primera versión del lenguaje Alloy apareció en 1997. Era un lenguaje de modelado de objetos bastante limitado . Las sucesivas iteraciones del lenguaje "agregaron cuantificadores , relaciones de aridad superior , polimorfismo , subtipificación y firmas". [2]
Los fundamentos matemáticos del lenguaje fueron fuertemente influenciados por la notación Z , y la sintaxis de Alloy debe más a lenguajes como Object Constraint Language .
El analizador de aleaciones se desarrolló específicamente para admitir los denominados "métodos formales ligeros". Como tal, está destinado a proporcionar un análisis completamente automatizado, en contraste con las técnicas interactivas de demostración de teoremas que se usan 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 booleano SAT . [1]
