You're viewing the readable version of this site. The interactive extras (search, diagrams, read-aloud) need JavaScript and a current browser. Enable JavaScript; if it is already enabled, update your browser.

Learn · All the Ways It Can Break

growing

A Small Scope Still Needs a Witness

Finite scope is a search boundary, and vacuity can make even exhaustive bounded analysis irrelevant.

formal-methods, alloy, scope, vacuity, authorization, learn

You will read global and exact scopes, expose two forms of vacuity, write an honest bounded result, and transfer the relational method to a new document-sharing graph without copying the worked relation.

Scope is a finite universe

A command such as for 5 but exactly 3 Principal sets a general upper bound and overrides one signature with an exact cardinality. Subsignature and one constraints further shape the universe. Record the complete command, not only the numeral after for.

Boundary — choose the claim that survives the finite scope.

Two vacuities

An implication passes when its antecedent is impossible. A security assertion also passes when the policy admits no readable document at all. Add runs for the antecedent and for useful behavior. If either is UNSAT, the assertion may be formally true but irrelevant to the intended system.

Increase and vary scopes after the smallest negative control. A defect that requires three distinct roles cannot appear in a two-principal universe. A property that passes several scopes remains bounded evidence unless a theorem or structural argument closes the gap.

Unlike transfer: sharing by grants

Build a new model with User, Document, and explicit Grant atoms carrying subject and object fields. Require revoked grants never authorize reads, while one active guest grant remains satisfiable. Do not copy Access.grants; the transfer deliberately changes a binary relation into reified grant objects.

Complete the lane only when the new model has:

  1. a SAT run for a useful active share;
  2. a SAT counterexample for a deliberately buggy revoked-grant rule;
  3. an UNSAT check for the repaired rule; and
  4. a result sentence naming every scope and forbidden inference.

Lessons

  • Scopes bound atoms and are refined by multiplicity and exact clauses.
  • Small-scope effectiveness is a heuristic, not a theorem.
  • Positive instances expose unreachable antecedents and deny-all repairs.
  • Varying scopes grows bounded evidence without making it unbounded.
  • Independent transfer demonstrates modeling ability better than editing the specimen.

Practice

  1. Retrieval. Explain for 5 but exactly 3 Principal.
  2. Discrimination. A check is UNSAT but its antecedent run is also UNSAT. What is the next action?
  3. Transfer. Complete the reified-grant model and grade every command before running it.

Worked answers

  1. Five is the general upper bound; Principal has exactly three atoms, with other declarations further constraining counts.
  2. Repair or relax the model until the intended antecedent has a witness; do not report the assertion as useful evidence yet.
  3. The expected polarity is SAT for useful sharing, SAT for the buggy check, and UNSAT for the fixed check within explicitly stated scopes.

References

  1. AlloyTools. Alloy tutorial. — scopes, instances, and analysis
  2. Daniel Jackson. Software Abstractions, Chapter 5. — small-scope analysis and validation

← Run Finds a World; Check Finds a Refutation Rust Can Be the Model →