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