Questions Concepts
GitHub icon

Alloy

Alloy - Programming language

< >

Alloy is a programming language created in 1997.

#303on PLDB 26Years Old 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.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

Language features

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

View source

- Build the next great programming language · Search · Add Language · Features · Creators · Resources · About · Blog · Acknowledgements · Queries · Stats · Sponsor · Traffic · Traffic Today · Day 305 · feedback@pldb.com · Logout