Alloy

En ciencia de los computadores e ingeniería informática, Alloy es un lenguaje de especificación declarativo para expresar complejas estructuras de control y comportamiento en un sistema software.Los soportes matemáticos del lenguaje fueron fuertemente influenciados por la notación Z, aunque la sintaxis de Alloy debe más a lenguajes tales como el lenguaje de control de objetos.[1]​ Alloy está orientado a la creación de micro-modelos que pueden ser automáticamente comprobados para su correctitud.La primera version del lenguaje Alloy apareció en 1997.Las sucesivas iteraciones del lenguaje "añadieron cuantificadores, mayores relaciones de aridad, polimorfismo, composición y firmas".