computer science Computer science is the study of computation, information, and automation. Computer science spans Theoretical computer science, theoretical disciplines (such as algorithms, theory of computation, and information theory) to Applied science, ...

and

software engineering Software engineering is a branch of both computer science and engineering focused on designing, developing, testing, and maintaining Application software, software applications. It involves applying engineering design process, engineering principl ...

, 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 exec ...

for expressing complex structural constraints and behavior in a

software system A software system is a system of intercommunicating software component, components based on software forming part of a computer system (a combination of Computer hardware, hardware and software). It "consists of a number of separate Computer progr ...

. Alloy provides a simple structural modeling tool based on

first-order logic First-order logic, also called predicate logic, predicate calculus, or quantificational logic, is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over ...

. 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 university, private research university in Cambridge, Massachusetts, United States. Established in 1861, MIT has played a significant role in the development of many areas of moder ...

in the

United States The United States of America (USA), also known as the United States (U.S.) or America, is a country primarily located in North America. It is a federal republic of 50 U.S. state, states and a federal capital district, Washington, D.C. The 48 ...

History and influences

The first version of the Alloy language appeared in 1997. It was a rather limited object modeling language. Succeeding iterations of the language "added quantifiers, higher

arity In logic, mathematics, and computer science, arity () is the number of arguments or operands taken by a function, operation or relation. In mathematics, arity may also be called rank, but this word can have many other meanings. In logic and ...

relations, polymorphism,

subtyping In programming language theory, subtyping (also called subtype polymorphism or inclusion polymorphism) is a form of type polymorphism. A ''subtype'' is a datatype that is related to another datatype (the ''supertype'') by some notion of substi ...

, 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 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 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. 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 variable (mathematics), variables are the truth values ''true'' and ''false'', usually denot ...

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 software Computer-related introductions in 1997 Formal specification languages Z notation