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 Applied science, practical discipli ...

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 A software system is a system of intercommunicating components based on software forming part of a computer system (a combination of hardware and software). It "consists of a number of separate programs, configuration files, which are used to se ...

. 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 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 th ...

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 Continental United States, primarily located in North America. It consists of 50 U.S. state, states, a Washington, D.C., ...

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 Arity () is the number of arguments or operands taken by a function, operation or relation in logic, mathematics, and computer science. In mathematics, arity may also be named ''rank'', but this word can have many other meanings in mathematics. ...

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 In linguistics, syntax () is the study of how words and morphemes combine to form larger units such as phrases and sentences. Central concerns of syntax include word order, grammatical relations, hierarchical sentence structure ( constituenc ...

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

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 edito ...

techniques commonly used with specification languages similar to Alloy. Development of the Analyzer was originally inspired by the automated analysis provided by model checkers. 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 In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisf ...

. 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 into a corresponding

boolean logic In mathematics and mathematical logic, Boolean algebra is a branch of algebra. It differs from elementary algebra in two ways. First, the values of the variables are the truth values ''true'' and ''false'', usually denoted 1 and 0, whereas ...

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 website

Alloy Github Repository

Guide to Alloy

Kodkod analysis engine website
at 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