Learn · All the Ways It Can Break

growing

Everything Begins as a Relation

Alloy models a world as atoms and tuples before it models algorithms.

formal-methods, alloy, relations, authorization, learn

You will create an Alloy 6.2.0 model from a blank file, declare signatures and a binary relation, read multiplicities, and separate an atom from a tuple and a set of tuples. Experienced readers can connect the syntax to first-order relational logic without skipping the concrete graph.

Name the atoms and tuples

Download the official Alloy 6.2.0 distribution and open a blank Sharing.als model. The checked specimen starts here:

alloy code/all-the-ways-it-can-break/document-sharing/Sharing.als#signatures Sharing.als grants is a binary relation from principals to documents.

If the application will not start, confirm that the downloaded package is the 6.2.0 build for the host platform before changing the model. If the Analyzer opens but reports syntax errors, first confirm that the editor contains a .als model rather than rendered page text and that the complete ruled snippet was copied. Tool startup and parsing must succeed before an instance or counterexample has any meaning.

abstract sig Principal says every principal atom belongs to a more specific subsignature. one sig creates exactly one atom of each named role in this model. Principal -> Document is the set of all ordered pairs with a principal on the left and a document on the right.

Prediction — read a field as mathematics rather than storage.

Multiplicity is part of the claim

one means exactly one, lone at most one, some at least one, and set places no additional cardinality restriction. Changing one sig Document to sig Document admits zero or more documents within the command's scope. Changing a field from set to one may silently assert that every principal has exactly one document.

Write multiplicities from the domain rule, not from the current database schema. An implementation column can be nullable while the intended model says every published object has exactly one owner—or the reverse.

A model describes permitted worlds

The declarations alone permit many grant relations. Predicates, facts, and assertions will narrow or question those worlds in later chapters. First make the carrier honest: identify atoms, relation arity, and multiplicity. If time, mutation, or order is part of the question, it must be modeled explicitly; Alloy does not infer a transition system from table-like syntax.

Lessons

Signatures introduce sets of atoms.
Fields introduce relations, represented as sets of tuples.
Multiplicity keywords are semantic constraints.
The Analyzer searches for complete finite worlds satisfying the formula.
Relational structure is not automatically temporal behavior.

Practice

Retrieval. Define atom, tuple, relation, and signature.
Discrimination. Should a document's owners be one or some if joint ownership is permitted but ownerless documents are forbidden?
Transfer. Declare users, groups, and a membership relation.

Worked answers

An atom is indivisible; a tuple is an ordered list of atoms; a relation is a set of same-arity tuples; a signature denotes a set of atoms.
some owners.
sig User {} sig Group { members: set User }.

References

AlloyTools. Alloy tutorial. — signatures, relations, and multiplicity
Daniel Jackson. Software Abstractions. MIT Press, 2012. — relational modeling and analysis

← Strengthen What Must Survive One Step Join Replaces the Pointer Chase →

An authorization graph is awkward to explain as a sequence of mutations. It is natural as a set of facts: these principals exist, these documents exist, and these principal-document pairs belong to the grant relation. Alloy begins there. A signature introduces atoms; a field introduces tuples among atoms. The scene is deliberately finite but not preconstructed. The Analyzer chooses an instance satisfying the constraints. That reversal matters: the model says what a permitted world must look like, and the tool finds a world—or proves none exists inside the declared scope.