Capstone — Applying Discrete Math to Real Programming Problems

"A user can access a resource if they're an admin, or they own the resource and it isn't locked" becomes Admin ∨ (Owner ∧ ¬Locked). When access is denied, a good error message needs the negation — applying De Morgan's Law directly: ¬(Admin ∨ (Owner ∧ ¬Locked)) ≡ ¬Admin ∧ (¬Owner ∨ Locked). That's precisely the reasoning a clear denial message would need: "not an admin, and either you don't own it or it's locked."

"Every admin can access every resource" becomes ∀u ∀r (Admin(u) → CanAccess(u, r)). This is directly testable: all(can_access(u, r) for u in admins for r in resources) is the code-level check of the exact same claim.

The resources visible to a given user are owned_by(user) ∪ (visible_to_admins if is_admin(user) else ∅) — a direct union of two sets, exactly Chapter 4's own operation, not a special case invented separately.

"Owns" is a relation between users and resources — but it isn't reflexive or symmetric, and doesn't need to be; not every relation has to be an equivalence relation. "Is on the same team as," by contrast, genuinely is one — reflexive, symmetric, and transitive — and its equivalence classes are exactly the teams themselves, the same GROUP BY connection Chapter 5 made directly.

The system's own get_user(user_id) function needs to be injective — no two different users may ever share an ID — or "the" user identified by a given ID becomes genuinely ambiguous. This isn't a stylistic preference; it's a correctness requirement for the entire system to even make sense, formalized exactly by Chapter 6's own definition.

Folders can be nested — if a user isn't directly permitted on a folder, the check recurses upward to the parent. Proving this recursive check is correct for a folder tree of any depth is exactly structural induction: base case, the root folder (no parent, checked directly); inductive step, assuming the check is correct for a subtree of depth k, it remains correct for depth k+1, since the recursive call on the parent is covered by the inductive hypothesis. Chapter 8's own reasoning, applied directly to a real recursive function.

The access rule from Step 1 combines three independent boolean conditions — Admin, Owner, Locked. By the multiplication principle, there are 2 × 2 × 2 = 8 distinct combinations to cover for full test coverage of the rule's own logic — a direct, practical answer to "how many test cases do I actually need here," not a guess.