Keep Documents Focused

One spec file should cover one feature or one bounded concern. Split by feature boundary, not by test type. Do not put "all Alloy models" in one file and "all executable blocks" in another. The value of specdown is that model and implementation verification live together.

Verification

• Valid instances — run generates concrete instances satisfying the model's constraints, confirming the model is consistent (not vacuously true). A run sanityCheck {} should accompany every model.
• Counterexample search — check automatically finds assertion violations. Counterexamples are saved as artifacts for debugging.
• Exhaustive coverage within scope — executable blocks test selected examples; Alloy proves properties for every combination of atoms up to the given scope.

Logical Relationship Discovery

• Equivalence — proving two models equivalent lets you reuse existing tests after a refactor (see Equivalence Shield).
• Implication — proving a strong invariant implies weaker properties eliminates the need to test those weaker properties separately (see Invariant Leverage).
• Vacuous satisfaction detection — if facts are contradictory, every assertion passes trivially. Alloy's instance finder exposes this trap.

Document Quality

• Design intent made precise — an Alloy model forces prose claims into formal statements. Ambiguous prose becomes a concrete predicate.
• Prose errors surfaced — when a property claimed in prose fails in the model, the counterexample reveals the inconsistency immediately.
• Missing constraints discovered — when an executable block finds a bug, adding the missing constraint to the model lets Alloy search for further violations (see Failure-Driven Modeling).

Test Optimization

• Exhaustive classification — proving a case partition is complete and mutually exclusive means one representative per case suffices (see Exhaustive Classification).
• Impossible transitions proved — modeling state machines lets Alloy prove which transitions cannot occur, reducing the invalid-path tests needed (see Transition Safety Net).
• Composition coverage — individual modules are tested with executable blocks; Alloy covers the combinatorial space of their interaction (see Composition Safety).

1. Property and Implementation Side by Side

Place an alloy:model block with a check statement and a check table in the same section. Readers see both the design guarantee and the implementation confirmation together. When a check exists in the model block, the HTML report links the result automatically — no alloy:ref needed.

Here is a minimal example — an Alloy model proves that every item has an owner, and a check table confirms the implementation enforces the same rule:

module ownership

sig User {}
sig Item { owner: one User }

assert everyItemHasOwner {
  all i: Item | one i.owner
}

check everyItemHasOwner for 5

2. Counterexample Harvesting

When Alloy finds a counterexample, fix the model, then add the counterexample as a check row to prevent regression. Document the counterexample in prose so future readers know why the row exists.

3. Exhaustive Classification

Use Alloy to prove the set of cases is complete and mutually exclusive, then test one representative per case. Two assertions — one for completeness, one for mutual exclusivity — together guarantee that the check table covers every case with minimal rows.

Here a permission model partitions access into three levels. Alloy proves every subject falls into exactly one level.

module classify

abstract sig Level {}
one sig Admin, Member, Guest extends Level {}

sig Subject { level: one Level }

pred isAdmin[s: Subject] { s.level = Admin }
pred isMember[s: Subject] { s.level = Member }
pred isGuest[s: Subject] { s.level = Guest }

-- completeness: every subject is one of the three
assert complete {
  all s: Subject | isAdmin[s] or isMember[s] or isGuest[s]
}

-- mutual exclusivity: no overlap
assert exclusive {
  no s: Subject | (isAdmin[s] and isMember[s])
    or (isMember[s] and isGuest[s])
    or (isAdmin[s] and isGuest[s])
}

check complete for 5
check exclusive for 5

With this proof, a check table needs only one representative per level (Admin, Member, Guest) — Alloy guarantees there are no gaps.

4. Invariant Leverage

Prove that one strong invariant implies several weaker properties. Then only test the strong invariant in implementation checks and skip the rest. Document why the weaker tests are absent — the Alloy proofs serve as the justification.

5. Transition Safety Net

Model state transitions in Alloy to prove which transitions are impossible. Executable blocks test the valid paths and a minimal set of invalid ones. No need to test every impossible pair; Alloy covers the rest.

See the State Machine Models section in the Alloy spec for a worked example.

6. Composition Safety

Test each module individually with executable blocks. Use Alloy to verify that their combination does not open unintended gaps. Testing every combination of states is impractical — Alloy covers the combinatorial space.

7. Failure-Driven Modeling

When an executable block discovers a bug, add the missing constraint to the Alloy model. Then let Alloy search for further violations. The cycle: implementation failure reveals a missing assumption, model is strengthened, Alloy finds more cases, new check rows are added.

8. Equivalence Shield

When refactoring, prove the old and new models are equivalent in Alloy. Then reuse existing executable blocks and check tables unchanged to confirm the implementation matches.

Vacuous satisfaction

If the model's facts are contradictory, every assertion passes trivially. Always include run sanityCheck {} for 5 to confirm the model has at least one instance. If it finds no instance, the model is inconsistent and all check results are meaningless.

Missing always in temporal models

In temporal Alloy (models with var fields), fact and assert bodies are evaluated in the initial state only. To express a constraint that must hold in every state, wrap the body with always.

Missing var when using prime

The prime operator (e') refers to the value of e in the next state. Without var, the field is static and e' = e always holds, making the assertion vacuously true.

Scope too small

check ... for 3 searches only instances with up to 3 atoms per signature. Properties that only fail with 4+ interacting elements will not be caught. Use a scope of 5-7 as a practical default. For temporal models, also set an adequate step bound (e.g. check ... for 5 but 8 steps).