In
computer science
Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to practical disciplines (includi ...
and
software engineering
Software engineering is a systematic engineering approach to software development.
A software engineer is a person who applies the principles of software engineering to design, develop, maintain, test, and evaluate computer software. The term '' ...
, Alloy is a declarative
specification language
A specification language is a formal language in computer science used during systems analysis, requirements analysis, and systems design to describe a system at a much higher level than a programming language, which is used to produce the execu ...
for expressing complex structural constraints and behavior in a
software system. Alloy provides a simple structural modeling tool based on
first-order logic
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
.
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 computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically associated with hardware or software systems ...
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
The Massachusetts Institute of Technology (MIT) is a private land-grant research university in Cambridge, Massachusetts. Established in 1861, MIT has played a key role in the development of modern technology and science, and is one of the ...
in the
United States
The United States of America (U.S.A. or USA), commonly known as the United States (U.S. or US) or America, is a country primarily located in North America. It consists of 50 states, a federal district, five major unincorporated territori ...
.
History and influences
The first version of the Alloy language appeared in 1997. It was a rather limited
object model
In computing, object model has two related but distinct meanings:
# The properties of objects in general in a specific computer programming language, technology, notation or methodology that uses them. Examples are the object models of ''Java'', ...
ing language. Succeeding iterations of the language "added
quantifiers, higher
arity relations,
polymorphism,
subtyping
In programming language theory, subtyping (also subtype polymorphism or inclusion polymorphism) is a form of type polymorphism in which a subtype is a datatype that is related to another datatype (the supertype) by some notion of substitutability, ...
, and signatures".
The mathematical underpinnings of the language were heavily influenced by the
Z notation
The Z notation is a formal specification language used for describing and modelling computing systems. It is targeted at the clear specification of computer programs and computer-based systems in general.
History
In 1974, Jean-Raymond Abria ...
, and the
syntax of Alloy owes more to languages such as
Object Constraint Language
The Object Constraint Language (OCL) is a declarative language describing rules applying to Unified Modeling Language (UML) models developed at IBM and is now part of the UML standard. Initially, OCL was merely a formal specification language ex ...
.
The Alloy Analyzer
![Screenshot of Alloy Analyzer](https://upload.wikimedia.org/wikipedia/commons/5/5e/Screenshot_of_Alloy_Analyzer.png)
The Alloy Analyzer was specifically developed to support so-called "lightweight formal methods". As such, it is intended to provide fully automated analysis, in contrast to the
interactive theorem proving
In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor ...
techniques commonly used with specification languages similar to Alloy. Development of the Analyzer was originally inspired by the automated analysis provided by
model checker
In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically associated with hardware or software system ...
s. However, model-checking is ill-suited to the kind of models that are typically developed in Alloy, and as a result the core of the Analyzer was eventually implemented as a model-finder built atop a
boolean SAT solver.
Through version 3.0, the Alloy Analyzer incorporated an integral SAT-based model-finder based on an off-the-shelf SAT-solver. However, as of version 4.0 the Analyzer makes use of the Kodkod model-finder, for which the Analyzer acts as a front-end. Both model-finders essentially translate a model expressed in
relational logic
In database theory, relational algebra is a theory that uses algebraic structures with a well-founded semantics for modeling data, and defining queries on it. The theory was introduced by Edgar F. Codd.
The main application of relational algebr ...
into a corresponding
boolean logic formula, and then invoke an off-the-shelf SAT-solver on the boolean formula. In the event that the solver finds a solution, the result is translated back into a corresponding binding of constants to variables in the relational logic model.
In order to ensure the model-finding problem is
decidable, the Alloy Analyzer performs model-finding over restricted scopes consisting of a user-defined finite number of objects. This has the effect of limiting the generality of the results produced by the Analyzer. However, the designers of the Alloy Analyzer justify the decision to work within limited scopes through an appeal to the ''small scope hypothesis'': that a high proportion of bugs can be found by testing a program for all test inputs within some small scope.
Model structure
Alloy models are relational in nature, and are composed of several different kinds of statements:
* Signatures define the vocabulary of a model by creating new sets
::
sig Object
defines a signature ''Object''
::
sig List
defines a signature ''List'' that contains a field ''head'' of type ''Node'' and multiplicity ''lone'' - this establishes the existence of a relation between ''List''s and ''Node''s such that every ''List'' is associated with no more than one head ''Node''
* Facts are constraints that are assumed to always hold
* Predicates are parameterized constraints, and can be used to represent operations
* Functions are expressions that return results
* Assertions are assumptions about the model
Because Alloy is a declarative language the meaning of a model is unaffected by the order of statements.
References
{{reflist
External links
Alloy websiteAlloy Github RepositoryGuide to AlloyKodkod analysis engine websiteat MIT
An Alloy Metamodel in Ecore
Formal methods tools
Satisfiability problems
Massachusetts Institute of Technology
Computer-related introductions in 1997
Formal specification languages
Z notation