Alloy is a programming language created in 1997.
| #301on PLDB | 26Years 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...
// 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 5module 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.name = e2.name => 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
| Feature | Supported | Token | Example |
|---|---|---|---|
| Integers | ✓ | // [0-9]+ |
|
| MultiLine Comments | ✓ | /* */ | /* A comment */ |
| Comments | ✓ | // A comment |
|
| Line Comments | ✓ | // | // A comment |
| Semantic Indentation | X |
| 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 |