A relational logic primer
In Alloy, constraints are specified in relational logic, an extension of firstorder logic with a few operators to compose relations. In this chapter we will present this logic in detail, namely detail the semantics of each of the operators, illustrated with several usage examples. These examples will be based on the file system specification introduced in chapter Structural design with Alloy, whose signatures and fields are detailed below.
abstract sig Object {}
sig File extends Object {}
sig Dir extends Object {
entries : set Entry
}
one sig Root extends Dir {}
sig Entry {
name : one Name,
object : one Object
}
sig Name {}
We will also use the following instance of this specification to illustrate the result of relational operators.
Occasionally we will also refer to the ternary relation
contents
used in the alternative version presented in
Using higherarity relations, whose content for the same instance of a file
system is depicted below.
Everything is a relation
Structures are described in Alloy using only (mathematical) relations. A relation is a set of tuples of objects drawn from the universe of discourse. Every tuple in a relation must have the same size, which is known as the arity of the relation.
For example, field name
is a relation of arity 2 (a binary
relation) relating entries with their names. For the above instance, it has four pairs, namely:
name = {(Entry0,Name0),(Entry1,Name2),(Entry2,Name1),(Entry3,Name1)}
In logic a relation is also known as a predicate, and the fact that
predicate name
holds for tuple (x,y)
is usually denoted
as name(x,y)
. As explained later, in Alloy this fact can be
denoted by x>y in name
.
An alternative way to depict a relation (or predicate) is using a
table, where each row corresponds to one of the tuples of the
relation. The table view of relation name
is depicted below.








This is also the standard way to present the value of relations in the Alloy Analyzer’s evaluator.
Relation contents
is a relation of arity 3 (a ternary
relation), relating directories, names, and objects. It contains four
triples, namely:
contents = {(Root,Name1,Dir0),(Root,Name0,File),(Root,Name2,File),(Dir0,Name1,Dir1)}
A set can also be represented by a relation of arity 1. In Alloy,
signatures are encoded in this way. For example, in the above
instance, signature Dir
has the value:
Dir = {(Root),(Dir0),(Dir1)}
Moreover, in Alloy even the constants and (quantified) variables are
represented by relations, namely singleton relations of arity 1. A
singleton is a relation with a single tuple. For example, signature
Root
, declared with multiplicity one
, has the following value.
Root = {(Root)}
Warning
Singleton signature names vs atom names.
Do not confuse the two occurrences of the word Root
in the
above definition. On the lefthand side, we have the signature
Root
that was declared in our specification to denote the root of
the file system. On the righthand side, we have the atom
Root
of the universe, whose name was automatically
generated by the Analyzer to populate signature Root
. The
name of this atom is actually irrelevant, but the Analyzer names
atoms using the signature name as prefix and a sequential number as
suffix. Actually, according to this naming convention, the name of
this atom is Root0
, and that is the name that will be
depicted in the evaluator if you ask for the value of signature
Root
. However, in the visualiser, if there is only a single
atom with a given name prefix the numeric suffix is omitted by default. In
this chapter we will use the names chosen by the visualiser.
Since atom names are arbitrary, when specifying constraints in Alloy it is impossible to refer to them directly. If we need to distinguish a particular atom of the universe, we need to declare a singleton signature that will contain that atom and refer to that signature name instead. That was precisely what we did to distinguish the root of a file system.
An instance of an Alloy specification without mutable declarations is a single snapshot with a complete valuation for all declared signatures and fields, mapping each of them to a relation of the appropriate arity. The value of all signatures and fields in our example instance is the following.
Object = {(Root),(Dir0),(Dir1),(File)}
Dir = {(Root),(Dir0),(Dir1)}
Root = {(Root)}
File = {(File)}
Entry = {(Entry0),(Entry1),(Entry2),(Entry3)}
Name = {(Name0),(Name1),(Name2)}
entries = {(Root,Entry0),(Root,Entry1),(Root,Entry2),(Dir0,Entry3)}
object = {(Entry0,File),(Entry1,File),(Entry2,Dir0),(Entry3,Dir1)}
name = {(Entry0,Name0),(Entry1,Name2),(Entry2,Name1),(Entry3,Name1)}
contents = {(Root,Name1,Dir0),(Root,Name0,File),(Root,Name2,File),(Dir0,Name1,Dir1)}
An instance also includes the values of the three predefined constants: none
(the empty set), univ
(the universe of all atoms), and iden
(the identity relation on the universe). In our example instance their value is the following.
none = {}
univ = {(Root),(Dir0),(Dir1),(File),(Entry0),(Entry1),(Entry2),(Entry3),(Name0),(Name1),(Name2)}
iden = {(Root,Root),(Dir0,Dir0),(Dir1,Dir1),(File,File),(Entry0,Entry0),(Entry1,Entry1),(Entry2,Entry2),(Entry3,Entry3),(Name0,Name0),(Name1,Name1),(Name2,Name2)}
Firstorder logic in a nutshell
Relational logic is an extension of firstorder logic, which in turn is an extension of propositional logic. In propositional logic the simplest (atomic) formula is a proposition that checks if a Boolean variable is true. Compound formulas can be built by connecting atomic formulas using the standard logic connectives (or operators): negation, conjunction, disjunction, implication, and equivalence. These connectives are also available in Alloy’s relational logic, and their syntax is the following.
Operator 
Name 

Negation 

Conjunction 

Disjunction 

Implication 

Equivalence 
As you can see, Alloy has a dual syntax for these operators, one with
programming language style symbols and the other with English
words. In this book we tend to use the latter, as the resulting
formulas are more readable. The implies
operator can also
have an optional else
to state what should be true when the
condition on the lefthand side is false. Given arbitrary formulas
P
, Q
, T
, P implies Q else T
is the
same as (P and Q) or (not P and T)
.
In firstorder logic we have a domain of discourse (or universe), and
propositions are generalised by predicates that relate elements of
this domain. Formulas can also be built using variables quantified
over this domain. There are two standard quantifiers: the universal
quantifier ∀ x . P
checks if a formula P
(possibly
referring to variable x
) is true for all x
in the
domain; and the existential quantifier ∃ x . P
checks if a
formula P
(possibly referring to variable x
) is true
for some x
in the domain. In Alloy all quantifications are
bounded by a set, and English words are
used instead of the standard mathematical notation. The following
table presents all quantifiers that are available in Alloy: A
is denotes an arbitrary set (a unary relation) and P
an arbitrary
formula. The first two are the standard universal and existential
quantifiers.
Quantifier 
Informal meaning 










It is well known that the existential quantifier can be specified with
the universal one, and viceversa, and the same is true for all other
Alloy quantifiers. For example, some x : A  P
is the same as
not (all x : A  not P)
and no x : A  P
is the same
as all x : A  not P
.
As mentioned above in Alloy everything is a relation. The same is true
for quantified variables: the quantified x
that can be
referred in P
is a unary relation containing a single tuple
with an atom of the universe. It is also possible to quantify more
than one variable at once, as in all x,y : A  P
or all
x : A, y : B  P
. In the latter, the expression B
can also refer to
the first quantified variable x
. It is
also possible to add keyword disj
to quantify over all different values of the bound variables.
For example, writing all disj x,y : A  P
abbreviates all x,y : A  x != y implies P
.
Besides predicates, firstorder logic also allows functions as
nonlogical symbols. Given some parameters a function returns an
element of the domain. Since in Alloy the atoms of the universe are
mostly uninterpreted there are very few predefined functions. The
exception is when using integers, for which we have the standard arithmetic
operations. If we do not consider functions, atomic formulas in
firstorder logic just check for equality of (quantified) variables or
if a tuple of (quantified) variables satisfies (or is a member of) a
predicate. In Alloy’s relational logic we have a few more atomic
formulas, that are described in the following table, where R
and S
are arbitrary relations of the same arity, including
sets.
Atomic formula 
Informal meaning 












The negation of the subset or equality atomic formulas can also be
written by placing the negation operator next to the comparison
operator. For example, instead of not (R in S)
it is possible
to write R not in S
or R !in S
.
Since quantified variables are also (singleton) relations, although in
stands for the subset or equal operator (\(⊆\)) it can also be used to
check set membership (∈
). As we will see below, given
variables x₁
, …, xₐ
, it is possible to define
expression x₁>…>xₐ
that denotes a relation with a single
tuple with those variables. Formula x₁>…>xₐ in R
can then
be used to check that this tuple belongs to a relation R
with
arity a
, something that in the standard mathematical notation
of firstorder logic is written as R(x₁,…,xₐ)
. Recall that,
besides equality checks between variables, such membership checks are
the only atomic formulas in firstorder logic. Although Alloy also
allows all the above ones, they all can be written using just these
basic checks, so technically they do not add expressive power to
firstorder logic, but just a more succinct way to write formulas. The
following table provides such formal definitions, assuming R
and S
have arity a
.
Atomic formula 
Formal meaning 












As we can see, the reduction in formula size can be substantial. For
example, to formalize the requirement that “every file is an object”,
in plain firstorder logic we would have to write ∀ x . File(x)
→ Object(x)
or, in Alloy’s notation, all x : univ  x in File
implies x in Object
. However, with Alloy’s relational logic we can
just write File in Object
.
Warning
Be careful with membership checks!
It is important to always recall that in
denotes the subset
operator and not the membership test. Of course, if we are certain
that the expression on the lefthand side is a singleton (a set
with a single tuple), in
behaves like membership. For
example, to test that Root
is a Dir
we can write
Root in Dir
. However, if the expression on the lefthand
side does not necessarily denote a singleton, this check may not
work as expected. For example, if Root
was declared with
multiplicity lone
instead of one
, the check
Root in Dir
will also be true if Root
is empty. In
this case, to be certain to test for membership you also need to
check that the lefthand expression is nonempty, as follows.
some Root and Root in Dir
Relational operators
As all the alternative atomic checks, most of the relational operators in Alloy do not technically add expressive power to firstorder logic, but just a more succinct alternative to write formulas. The full list of operators is presented below.
Operator 
Name 

Union 

Intersection 

Difference 

Composition, Dot join 

Box join 

(Cartesian) Product 

Domain restriction 

Range restriction 

Override 

Transpose, Converse 

Transitive closure 

Reflexive transitive closure 
These operators act like combinators, that can be used to put together relations
(predicates) to obtain expressions denoting more complex relations. The
most basic operators are the standard set operators of union,
intersection, and difference. For example, given predicates
File
and Dir
we can compose them with union to obtain
the derived predicate File + Dir
that can be used to directly
check if an element is either a file or a directory. This simplifies
the writing of requirements such as “every object is either a file or
a directory”. In plain firstorder logic we would write (using Alloy’s syntax):
all x : univ  x in Object implies x in File or x in Dir
By using the union operator we can simplify this to:
all x : univ  x in Object implies x in File + Dir
And finally by using the subset operator we can write just:
Object in File + Dir
Below we present the formal semantics of all relational operators in terms of plain firstorder logic. The formula in the right column formally specifies when a tuple belongs to an expression that uses each operator. To abbreviate, in this formula all variables are implicitly universally quantified over the universe. Notice that some of these operators (namely the transpose and the closure operators) are only defined for binary relations.
Operator 
Formal meaning 
























In the remainder of this section we will illustrate each operator with examples based on the file system specification presented above.
Composition
The entries inside the root
Root.entries = {(Root)}.{(Root,Entry0),(Root,Entry1),(Root,Entry2),(Dir0,Entry3)} = {(Entry0),(Entry1),(Entry2)}
The names of the entries inside the root
Root.entries.name = {(Entry0),(Entry1),(Entry2)}.name = {(Entry0),(Entry1),(Entry2)}.{(Entry0,Name0),(Entry1,Name2),(Entry2,Name1),(Entry3,Name1)} = {(Name0),(Name2),(Name1)}
The binary relation between directories and the contained objects
entries.object = {(Root,Entry0),(Root,Entry1),(Root,Entry2),(Dir0,Entry3)}.{(Entry0,File),(Entry1,File),(Entry2,Dir0),(Entry3,Dir1)} = {(Root,File),(Root,Dir0),(Dir0,Dir1)}
Nonempty directories
entries.Entry = {(Root,Entry0),(Root,Entry1),(Root,Entry2),(Dir0,Entry3)}.{(Entry0),(Entry1),(Entry2),(Entry3)} = {(Root),(Dir0)}
(contents.Object).Name = ({(Root,Name1,Dir0),(Root,Name0,File),(Root,Name2,File),(Dir0,Name1,Dir1)}.{(Root),(Dir0),(Dir1),(File)}).Name = {(Root,Name1),(Root,Name0),(Root,Name2),(Dir0,Name1)}.Name = {(Root,Name1),(Root,Name0),(Root,Name2),(Dir0,Name1)}.{(Name0),(Name1),(Name2)} = {(Root),(Dir0)}
Set operators
All directories except the root
Dir  Root = {(Root),(Dir0),(Dir1)}  {(Root)} = {(Dir0),(Dir1)}
The directories inside the root
Root.entries.object & Dir = Root.{(Root,File),(Root,Dir0),(Dir0,Dir1)} & Dir = {(File),(Dir0)} & {(Root),(Dir0),(Dir1)} = {(Dir0)}
Cartesian product
All possible associations between files and names
File>Name = {(File)} > {(Name0),(Name1),(Name3)} = {(File,Name0),(File,Name1),(File,Name3)}
Domain and range restriction
The identity relation on objects
Object <: iden = {(Root),(Dir0),(Dir1),(File)} <: {(Root,Root),(Dir0,Dir0),(Dir1,Dir1),(File,File),(Entry0,Entry0),(Entry1,Entry1),(Entry2,Entry2),(Entry3,Entry3),(Name0,Name0),(Name1,Name1),(Name2,Name2)} = {(Root,Root),(Dir0,Dir0),(Dir1,Dir1),(File,File)}
Override
A modified entries relation where all files are removed from the root directory
entries ++ (Root > (Root.entries & object.Dir)) = entries ++ (Root > ({(Root)}.{(Root,Entry0),(Root,Entry1),(Root,Entry2),(Dir0,Entry3)} & object.Dir)) = entries ++ (Root > ({(Entry0),(Entry1),(Entry2)} & object.Dir)) = entries ++ (Root > ({(Entry0),(Entry1),(Entry2)} & {(Entry0,File),(Entry1,File),(Entry2,Dir0),(Entry3,Dir1)}.{(Root),(Dir0),(Dir1)})) = entries ++ (Root > ({(Entry0),(Entry1),(Entry2)} & {(Entry2),(Entry3)})) = entries ++ (Root > {(Entry2)}) = entries ++ ({(Root)} > {(Entry2)}) = entries ++ ({(Root,Entry2)}) = {(Root,Entry0),(Root,Entry1),(Root,Entry2),(Dir0,Entry3)} ++ ({(Root,Entry2)}) = {(Root,Entry2),(Dir0,Entry3)}
Transpose
The binary relation between objects (contained in directories) and their name
~object.name = ~{(Entry0,File),(Entry1,File),(Entry2,Dir0),(Entry3,Dir1)}.{(Entry0,Name0),(Entry1,Name2),(Entry2,Name1),(Entry3,Name1)} = {(File,Entry0),(File,Entry1),(Dir0,Entry2),(Dir1,Entry3)}.{(Entry0,Name0),(Entry1,Name2),(Entry2,Name1),(Entry3,Name1)} = {(File,Name0),(File,Name2),(Dir0,Name1),(Dir1,Name1)} ~(Object.contents) = ~({(Root),(Dir0),(Dir1),(File)}.{(Root,Name1,Dir0),(Root,Name0,File),(Root,Name2,File),(Dir0,Name1,Dir1)}) = ~{(Name1,Dir0),(Name0,File),(Name2,File),(Name1,Dir1)} = {(File,Name0),(File,Name2),(Dir0,Name1),(Dir1,Name1)}
The binary relation between entries in the same directory
~entries.entries = ~{(Root,Entry0),(Root,Entry1),(Root,Entry2),(Dir0,Entry3)}.{(Root,Entry0),(Root,Entry1),(Root,Entry2),(Dir0,Entry3)} = {(Entry0,Root),(Entry1,Root),(Entry2,Root),(Entry3,Dir0)}.{(Root,Entry0),(Root,Entry1),(Root,Entry2),(Dir0,Entry3)} = {(Entry0,Entry0),(Entry0,Entry1),(Entry0,Entry2),(Entry1,Entry0),(Entry1,Entry1),(Entry1,Entry2),(Entry2,Entry0),(Entry2,Entry1),(Entry2,Entry2),(Entry3,Entry3)}
The binary relation between entries sharing names
name.~name = {(Entry0,Name0),(Entry1,Name2),(Entry2,Name1),(Entry3,Name1)}.~{(Entry0,Name0),(Entry1,Name2),(Entry2,Name1),(Entry3,Name1)} = {(Entry0,Name0),(Entry1,Name2),(Entry2,Name1),(Entry3,Name1)}.{(Name0,Entry0),(Name2,Entry1),(Name1,Entry2),(Name1,Entry3)} = {(Entry0,Entry0),(Entry1,Entry1),(Entry2,Entry2),(Entry2,Entry3),(Entry3,Entry2),(Entry3,Entry3)}
Closures
The binary relation between a directory and the objects contained in that directory or any subdirectory
^(entries.object) = ^{(Root,File),(Root,Dir0),(Dir0,Dir1)} = {(Root,File),(Root,Dir0),(Root,Dir1),(Dir0,Dir1)}
All objects in the file system
Root.*(entries.object) = Root.(^(entries.object) + iden) = Root.({(Root,File),(Root,Dir0),(Root,Dir1),(Dir0,Dir1)} + iden) = {(Root)}.{(Root,File),(Root,Dir0),(Root,Dir1),(Dir0,Dir1),(Root,Root),(Dir0,Dir0),(Dir1,Dir1),(File,File),(Entry0,Entry0),(Entry1,Entry1),(Entry2,Entry2),(Entry3,Entry3),(Name0,Name0),(Name1,Name1),(Name2,Name2)} = {(Root),(Dir0),(Dir1),(File)}
Set comprehension
The binary relation between directories and the contained objects
{ d : Dir, o : Object  some d.contents.o } = {(Root,File),(Root,Dir0),(Dir0,Dir1)}
Note
A question of style!
An object is not contained in more one entry, or relation content
is injective.
The pure firstorder (or pointwise) style.
all x,y : Entry, o : Object  x>o in object and y>o in object implies x=y
The most common Alloy navigational style.
all o : Object  lone object.o
The pure relational (or pointfree) style.
object.~object in iden
A typesystem for relational specifications
Caution
This section is still under construction