Menu
Home
People
Places
Arts
History
Plants & Animals
Science
Life & Culture
Technology
Reference.org
Alloy (specification language)
open-in-new
<h2 id="history-and-influences">History and influences</h2> <p>The first version of the Alloy language appeared in 1997. It was a rather limited <a href="/facts/Object_model/sAjjBb7V">object modeling</a> language. Succeeding iterations of the language "added <a href="/facts/Quantifier_(logic)/bgmvwxoo">quantifiers</a>, higher <a href="/facts/Arity/zSVuwHvP">arity</a> relations, <a href="/facts/Polymorphism_(computer_science)/S3cCKsVT">polymorphism</a>, <a href="/facts/Subtyping/0L9t8twv">subtyping</a>, and signatures".<a class="footnote-ref" id="fnref:2" href="#fn:2"><sup>2</sup></a> </p><p>The mathematical underpinnings of the language were heavily influenced by the <a href="/facts/Z_notation/5mUjpTvv">Z notation</a>, and the <a href="/facts/Syntax/6PxSV98p">syntax</a> of Alloy owes more to languages such as <a href="/facts/Object_Constraint_Language/coIhRpJb">Object Constraint Language</a>. </p> <h2 id="the-alloy-analyzer">The Alloy Analyzer</h2> <p>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 <a href="/facts/Proof_assistant/hjFGxLPn">interactive theorem proving</a> techniques commonly used with specification languages similar to Alloy. Development of the Analyzer was originally inspired by the automated analysis provided by <a href="/facts/Model_checker/FwvKMlw9">model checkers</a>. 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 <a href="/facts/Boolean_satisfiability_problem/wBVRjWoy">boolean SAT solver</a>.<a class="footnote-ref" id="fnref:3" href="#fn:3"><sup>3</sup></a> </p><p>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 <a href="/facts/Relational_logic/7tjTFXdf">relational logic</a> into a corresponding <a href="/facts/Boolean_logic/VkCToAmg">boolean logic</a> 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.<a class="footnote-ref" id="fnref:4" href="#fn:4"><sup>4</sup></a> </p><p>In order to ensure the model-finding problem is <a href="/facts/Decidability_(logic)/17SHPMo0">decidable</a>, 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 <i>small scope hypothesis</i>: that a high proportion of bugs can be found by testing a program for all test inputs within some small scope.<a class="footnote-ref" id="fnref:5" href="#fn:5"><sup>5</sup></a> </p> <h2 id="model-structure">Model structure</h2> <p>Alloy models are relational in nature, and are composed of several different kinds of statements:<a class="footnote-ref" id="fnref:6" href="#fn:6"><sup>6</sup></a> </p> <ul><li>Signatures define the vocabulary of a model by creating new sets</li></ul> sig Object{} defines a signature <i>Object</i> sig List{ head : lone Node } defines a signature <i>List</i> that contains a field <i>head</i> of type <i>Node</i> and multiplicity <i>lone</i> - this establishes the existence of a relation between <i>List</i>s and <i>Node</i>s such that every <i>List</i> is associated with no more than one head <i>Node</i> <ul><li>Facts are constraints that are assumed to always hold</li> <li>Predicates are parameterized constraints, and can be used to represent operations</li> <li>Functions are expressions that return results</li> <li>Assertions are assumptions about the model</li></ul> <p>Because Alloy is a declarative language the meaning of a model is unaffected by the order of statements. </p> <h2 id="external-links">External links</h2> <ul><li><a href="https://alloytools.org/">Alloy website</a></li> <li><a href="https://github.com/AlloyTools/org.alloytools.alloy">Alloy Github Repository</a></li> <li><a href="http://www.doc.ic.ac.uk/project/examples/2007/271j/suprema_on_alloy/Web/">Guide to Alloy</a></li> <li><a href="https://web.archive.org/web/20090302204321/http://alloy.mit.edu/kodkod/">Kodkod analysis engine website</a> at MIT</li> <li><a href="https://web.archive.org/web/20160304195131/http://www.irisa.fr/triskell/Software/pramana/AlloyMetamodel/Alloy.ecore">An Alloy Metamodel in Ecore</a></li></ul> <h2 id="references">References</h2> <ol> <li id="fn:1"><p>Jackson, Daniel (2006). Software Abstractions: Logic, Language, and Analysis. MIT Press. ISBN 978-0-262-10114-1. <a href="978-0-262-10114-1" target="_blank">978-0-262-10114-1</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></p></li> <li id="fn:2"><p>"Alloy FAQ". Archived from the original on 7 June 2007. Retrieved 7 March 2013. <a href="https://web.archive.org/web/20070607115911/http://alloy.mit.edu/faq.php" target="_blank">https://web.archive.org/web/20070607115911/http://alloy.mit.edu/faq.php</a> <a href="#fnref:2" class="footnote-back-ref">↩</a></p></li> <li id="fn:3"><p>Jackson, Daniel (2006). Software Abstractions: Logic, Language, and Analysis. MIT Press. ISBN 978-0-262-10114-1. <a href="978-0-262-10114-1" target="_blank">978-0-262-10114-1</a> <a href="#fnref:3" class="footnote-back-ref">↩</a></p></li> <li id="fn:4"><p>Torlak, E.; Dennis, G. (April 2008). "Kodkod for Alloy Users" (PDF). First ACM Alloy Workshop. Portland, Oregon. Archived from the original (PDF) on 22 June 2010. Retrieved 19 April 2009. <a href="/wiki/Emina_Torlak" target="_blank">/wiki/Emina_Torlak</a> <a href="#fnref:4" class="footnote-back-ref">↩</a></p></li> <li id="fn:5"><p>Andoni, Alexandr; Daniliuc, Dumitru; Khurshid, Sarfraz; Marinov, Darko (2002). "Evaluating the small scope hypothesis". CiteSeerX 10.1.1.8.7702. <a href="/wiki/CiteSeerX_(identifier)" target="_blank">/wiki/CiteSeerX_(identifier)</a> <a href="#fnref:5" class="footnote-back-ref">↩</a></p></li> <li id="fn:6"><p>Jackson, Daniel (2006). Software Abstractions: Logic, Language, and Analysis. MIT Press. ISBN 978-0-262-10114-1. <a href="978-0-262-10114-1" target="_blank">978-0-262-10114-1</a> <a href="#fnref:6" class="footnote-back-ref">↩</a></p></li> </ol>