Learn · All the Ways It Can Break
growing
Join Replaces the Pointer Chase
Relational composition asks who can reach what without embedding traversal order in the model.
You will evaluate binary joins by hand, use set operators and quantifiers, and recognize when transitive closure is the right question. You will also detect the common column-order mistake that produces a valid but unintended formula.
Match the middle column
If grants contains Guest -> Document, then Guest.(Access.grants) yields Document. More generally, joining A -> B with B -> C yields A -> C. The matching B column disappears.
Policies are set constraints
The specimen's policies are short because the carrier does the work:
alloy code/all-the-ways-it-can-break/document-sharing/Sharing.als#policies Sharing.als The broken relation grants the full cross product. The fixed relation restricts its left column while retaining a useful owner tuple.
in means subset when both sides are sets. Owner + Guest is union. - is difference and & intersection. Quantifiers such as all p: Principal | and some d: Document | range over the finite instance selected by the command.
Closure asks about paths
For a homogeneous relation edge: Node -> Node, ^edge is nonempty transitive closure and *edge is reflexive-transitive closure. Use closure when the claim concerns paths of arbitrary length within the finite instance. Do not use it merely to imitate a loop. The relation's direction and whether a zero-length path counts are part of the claim.
Under the hood: column types catch some, not all, mistakes
Alloy rejects many impossible joins by type. But when both columns have the same signature, reversing a relation may remain well typed while changing its meaning. Construct a three-atom instance by hand and compute the intended tuples before trusting a compact expression.
Lessons
- Join composes relations by matching adjacent columns.
- Field-like dot syntax remains relational composition.
- Set operators constrain whole tuple sets.
- Closure expresses reachability, with or without zero-length paths.
- A well-typed join can still use the wrong direction.
Practice
- Retrieval. What happens to the matched column during join?
- Discrimination. Use
^edgeor*edgeto ask whether a node can reach itself without moving? - Transfer. Express documents readable through direct grants or group ownership.
Worked answers
- It is matched and removed from the result.
*edge, because reflexive closure includes zero steps.user.direct + user.membership.ownsfor suitably typed relations.
References
- AlloyTools. Alloy tutorial. — relational operators, quantifiers, and closure
- Daniel Jackson. Software Abstractions, Chapters 2–4. — relational logic by construction