Alloy (specification language)
Encyclopedia
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
. The mathematical underpinnings of the language were heavily influenced by the Z notation
, although the syntax
of Alloy owes more to languages such as Object Constraint Language
. 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.
The first version of the Alloy language appeared in 1997. It was a rather limited object model
ing language. Succeeding iterations of the language "added quantifiers, higher arity
relations, polymorphism, subtyping, and signatures". 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.
Because Alloy is a declarative language the meaning of a model is unaffected by the order of statements.
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
and software engineering
Software engineering
Software Engineering is the application of a systematic, disciplined, quantifiable approach to the development, operation, and maintenance of software, and the study of these approaches; that is, the application of engineering to software...
, Alloy is a declarative specification language
Specification language
A specification language is a formal language used in computer science.Unlike most programming languages, which are directly executable formal languages used to implement a system, specification languages are used during systems analysis, requirements analysis and systems design.Specification...
for expressing complex structural constraints and behavior in a software system
Software system
A software system is a system based on software forming part of a computer system . The term "software system" is often used as a synonym of computer program or software; is related to the application of systems theory approaches in software engineering context and are used to study large and...
. Alloy provides a simple structural modeling tool based on first-order logic
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
. The mathematical underpinnings of the language were heavily influenced by the Z notation
Z notation
The Z notation , named after Zermelo–Fraenkel set theory, 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:...
, although the syntax
Syntax
In linguistics, syntax is the study of the principles and rules for constructing phrases and sentences in natural languages....
of Alloy owes more to languages such as Object Constraint Language
Object Constraint Language
The Object Constraint Language is a declarative language for describing rules that apply to Unified Modeling Language models developed at IBM and now part of the UML standard. Initially, OCL was only a formal specification language extension to UML. OCL may now be used with any Meta-Object...
. 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.
The first version of the Alloy language appeared in 1997. It was a rather limited object model
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. For example, the Java objects model, the COM object model, or the object model of OMT...
ing language. Succeeding iterations of the language "added quantifiers, higher arity
Arity
In logic, mathematics, and computer science, the arity of a function or operation is the number of arguments or operands that the function takes. The arity of a relation is the dimension of the domain in the corresponding Cartesian product...
relations, polymorphism, subtyping, and signatures". 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.
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 Objectsig List{ head : lone Node }defines a signature List that contains a field head of type Node and multiplicity lone - this establishes the existence of a relation between Lists and Nodes 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 that can be checked using the Alloy Analyzer
Because Alloy is a declarative language the meaning of a model is unaffected by the order of statements.