Topic | v1 | created by jjones |

In computer science and software engineering, Alloy is a declarative specification language for expressing complex structural constraints and behavior in a software system. Alloy provides a simple structural modeling tool based on first-order logic. Alloy is targeted at the creation of micro-models that can then be automatically checked for correctness. Alloy specifications can be checked using the Alloy Analyzer. Although Alloy is designed with automatic analysis in mind, Alloy differs from many specification languages designed for model-checking in that it permits the definition of infinite models. The Alloy Analyzer is designed to perform finite scope checks even on infinite models. The Alloy language and analyzer are developed by a team led by Daniel Jackson at the Massachusetts Institute of Technology in the United States.


is Programming language

A programming language is a formal language comprising a set of instructions that produce various kin...

Edit details Edit relations Attach new author Attach new topic Attach new resource

treated in Alloy 4 cheat sheet

8.0 rating 5.0 level 8.0 clarity 3.0 background – 1 rating

Alloy 4 quick reference summary by C. M. SperbergMcQueen, Black Mesa Technologies LLC. ©2013 CC-BYSA...

treated in Formal methods

In this course, we will study a collection of techniques that are essential in the construction of la...