Alloy is an actively used programming language created in 1997.

22Years Old 1,025Users 0Jobs

Example code 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 code 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
Edit

Last updated February 11th, 2019