Languages Features Calendar CSV Lists Blog About Sponsor Add Language
GitHub icon



Alloy is a pl created in 1997.

#300on PLDB 25Years Old 376Users
0Books 13Papers 759Repos

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. Alloy is targeted at the creation of micro-models that can then be automatically checked for correctness. Read more on Wikipedia...

Example from the web:
// A file system object in the file system sig FSObject { parent: lone Dir } // A directory in the file system sig Dir extends FSObject { contents: set FSObject } // A file in the file system sig File extends FSObject { } // A directory is the parent of its contents fact { all d: Dir, o: d.contents | o.parent = d } // All file system objects are either files or directories fact { File + Dir = FSObject } // There exists a root one sig Root extends Dir { } { no parent } // File system is connected fact { FSObject in Root.*contents } // The contents path is acyclic assert acyclic { no d: Dir | d in d.^contents } // Now check it for a scope of 5 check acyclic for 5 // File system has one root assert oneRoot { one d: Dir | no d.parent } // Now check it for a scope of 5 check oneRoot for 5 // Every fs object is in at most one directory assert oneLocation { all o: FSObject | lone d: Dir | o in d.contents } // Now check it for a scope of 5 check oneLocation for 5
Example from Linguist:
module examples/systems/file_system /* * Model of a generic file system. */ abstract sig Object {} sig Name {} sig File extends Object {} { some d: Dir | this in d.entries.contents } sig Dir extends Object { entries: set DirEntry, parent: lone Dir } { parent = this.~@contents.~@entries all e1, e2 : entries | = => e1 = e2 this !in this.^@parent this != Root => Root in this.^@parent } one sig Root extends Dir {} { no parent } lone sig Cur extends Dir {} sig DirEntry { name: Name, contents: Object } { one this.~entries } /** * all directories besides root have one parent */ pred OneParent_buggyVersion { all d: Dir - Root | one d.parent } /** * all directories besides root have one parent */ pred OneParent_correctVersion { all d: Dir - Root | (one d.parent && one contents.d) } /** * Only files may be linked (that is, have more than one entry) * That is, all directories are the contents of at most one directory entry */ pred NoDirAliases { all o: Dir | lone o.~contents } check { OneParent_buggyVersion => NoDirAliases } for 5 expect 1 check { OneParent_correctVersion => NoDirAliases } for 5 expect 0

Language features

Feature Supported Example Token
// [0-9]+
MultiLine Comments
/* A comment
/* */
// A comment
Line Comments
// A comment
Semantic Indentation ϴ

Publications about Alloy from Semantic Scholar

title authors year citations influentialCitations
Automated Test Generation and Mutation Testing for Alloy Allison Sullivan and Kaiyuan Wang and Razieh Nokhbeh Zaeem and S. Khurshid 2017 32 1
Verification of Aspect-UML models using alloy Farida Mostefaoui and J. Vachon 2007 24 1
αRby - An Embedding of Alloy in Ruby Aleksandar Milicevic and I. Efrati and D. Jackson 2014 16 3
Towards a test automation framework for alloy Allison Sullivan and Razieh Nokhbeh Zaeem and S. Khurshid and D. Marinov 2014 15 1
Generators and the replicator control structure in the parallel environment of ALLOY Thanasis Mitsolides and M. Harrison 1990 9 0
An Automated Approach for Writing Alloy Specifications Using Instances S. Khurshid and Muhammad Zubair Malik and Engin Uzuncaova 2006 5 1
FLACK: Counterexample-Guided Fault Localization for Alloy Models Guolong Zheng and ThanhVu Nguyen and Simón Gutiérrez Brida and Germán Regis and M. Frias and Nazareno Aguirre and H. Bagheri 2021 4 0
Bounded Exhaustive Search of Alloy Specification Repairs Simón Gutiérrez Brida and Germán Regis and Guolong Zheng and H. Bagheri and ThanhVu Nguyen and Nazareno Aguirre and M. Frias 2021 4 0
Numerical simulation of laser powder deposition for TC15 titanium alloy brick parts J. Cheng 2014 3 1
Discrete mathematics for computing students: A programming oriented approach with Alloy Leo C. Ureel and C. Wallace 2016 3 0
Quantitative Characterization of Pore Arrangement in Pore Bands in Pressure Die Cast AZ91 Magnesium Alloy by Image Processing D. Prakash and D. Regener 2006 2 0
Lab exercises for a discrete structures course: exploring logic and relational algebra with Alloy L. E. Brown and Adam Feltz and C. Wallace 2018 1 0
A Labview/Arduino Measurement System for Shape Memory Alloy Wires J. Driesen and Clécio Fischer and Guilherme L. Caselato de Sousa and O. Santos and R. Loendersloot and D. Rade and Cristiane Aparecida Martins and L. Góes 2018 1 0
foxpro.html · alloy.html · intercal.html

View source

PLDB - Build the next great programming language · v2022 · Day 31 · Docs · Build · Acknowledgements · Traffic Today · Traffic Trends · Mirrors · GitHub ·