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] La aleación 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 con 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 .
Historia e influencias
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
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 totalmente 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]
A través de la versión 3.0, el Alloy Analyzer incorporó un buscador de modelos integral basado en SAT basado en un solucionador SAT listo para usar. Sin embargo, a partir de la versión 4.0, el Analizador hace uso del buscador de modelos Kodkod, para el cual el Analizador 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 el caso de que el solucionador encuentre una solución, el resultado se traduce de nuevo en un enlace correspondiente de constantes a variables en el modelo lógico relacional. [3]
Para garantizar que el problema de búsqueda de modelos sea decidible , el Alloy Analyzer realiza la búsqueda de modelos en ámbitos restringidos que constan de 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]
Estructura del modelo
Los modelos de aleación son de naturaleza relacional y se componen de varios tipos diferentes de declaraciones: [1]
- Las firmas definen el vocabulario de un modelo creando nuevos conjuntos
sig Object{}define un objeto de firmasig List{ head : lone Node }define una lista de firmas que contiene un encabezado de campo de tipo Nodo y multiplicidad solo : esto establece la existencia de una relación entre las listas y los nodos de manera que cada lista está asociada con no más de un nodo principal
- Los hechos son restricciones que se supone que siempre son válidas.
- Los predicados son restricciones parametrizadas y se pueden usar para representar operaciones
- Las funciones son expresiones que devuelven resultados
- Las afirmaciones son suposiciones sobre el modelo.
Debido a que Alloy es un lenguaje declarativo, el significado de un modelo no se ve afectado por el orden de las declaraciones.
Referencias
- ↑ a b c Jackson, Daniel (2006). Abstracciones de software: lógica, lenguaje y análisis . Prensa del MIT . ISBN 978-0-262-10114-1.
- ^ "Preguntas frecuentes sobre aleación" . Archivado desde el original el 7 de junio de 2007 . Consultado el 7 de marzo de 2013 .
- ↑ Torlak, E .; Dennis, G. (abril de 2008). "Kodkod para usuarios de aleación" (PDF) . Primer Taller de Aleaciones ACM . Portland, Oregon. Archivado desde el original (PDF) el 22 de junio de 2010 . Consultado el 19 de abril de 2009 .
- ^ Andoni, Alexandr; Daniliuc, Dumitru; Khurshid, Sarfraz; Marinov, Darko (2002). "Evaluación de la hipótesis de pequeño alcance". CiteSeerX 10.1.1.8.7702 . Cite journal requiere
|journal=( ayuda )
Enlaces externos
- Sitio web de Alloy
- Repositorio de Alloy Github
- Guía de aleación
- Sitio web del motor de análisis Kodkod en el MIT
- Un metamodelo de aleación en Ecore
