Module 1: Proofs & Discrete Structures: Case Studies
These cases make proof work practical: define the claim, expose assumptions, and produce a checkable argument.
Case Study 1: Proving an API Invariant
Scenario: A rate limiter should never allow more than ` requests in a window. Tests pass on examples, but the team needs an argument that the invariant holds for all request sequences.
Source anchor: MIT Mathematics for Computer Science.
Module concepts:
- invariants
- universal claims
- proof by induction
- counterexamples
Wrong Approach
List several example sequences and call that a proof.
Better Approach
State the invariant precisely, prove it holds initially, then prove each operation preserves it. Separately test edge cases to catch implementation mistakes.
Tradeoff Table
| Choice | Gain | Cost |
|---|---|---|
| Examples only | Easy confidence | Not a proof |
| Inductive invariant | General assurance | Requires precise state |
| Formal verification | Stronger guarantee | Higher tool cost |
Failure Mode
An untested request ordering violates the limit.
Required Artifact
Write the invariant, base case, inductive step for add/expire operations, and one counterexample to a weaker invariant.
Project / Capstone Connection
Use this invariant-writing style later when defending rate limits, state machines, or data-structure correctness in project artifacts.
Case Study 2: Set Operations in Permission Design
Scenario: A permissions system combines roles, explicit grants, and explicit denies. A developer treats "not granted" as "denied" and breaks inherited access.
Source anchor: MIT Mathematics for Computer Science.
Module concepts:
- sets
- union and intersection
- complements
- logical implication
Wrong Approach
Mix boolean flags without defining the universe of permissions.
Better Approach
Define permission sets: granted by role, granted directly, denied directly, and effective permissions. Specify precedence and compute with set operations.
Tradeoff Table
| Choice | Gain | Cost |
|---|---|---|
| Boolean flags | Quick to add | Ambiguous combinations |
| Set model | Clear semantics | Requires careful universe definition |
| Policy engine | Flexible rules | More infrastructure |
Failure Mode
A user loses access because absence of a grant is confused with an explicit deny.
Required Artifact
Create a set-definition table and evaluate three users with different grant/deny combinations.
Project / Capstone Connection
Reuse set-definition tables in later authorization, tagging, dependency, and feature-flag models where inclusion rules matter.
Case Study 3: Contrapositive in Input Validation
Scenario: A validation rule says: if a request is accepted, then it has a valid signature. A learner tries to prove it directly but keeps reasoning from rejected requests.
Source anchor: MIT Mathematics for Computer Science.
Module concepts:
- implication
- contrapositive
- necessary vs sufficient conditions
- proof structure
Wrong Approach
Assume "invalid signature implies rejected" is the same as every related statement.
Better Approach
Use the contrapositive carefully: if the signature is invalid, the request is not accepted. Keep converse and inverse statements separate.
Tradeoff Table
| Choice | Gain | Cost |
|---|---|---|
| Direct proof | Natural if simple | May be awkward |
| Contrapositive | Often clearer | Easy to confuse with converse |
| Examples | Helpful intuition | Cannot establish all cases |
Failure Mode
The learner proves a different statement than the security claim.
Required Artifact
Write the original claim, converse, inverse, contrapositive, and mark which are equivalent.
Project / Capstone Connection
Bring this claim-separation discipline into later design reviews so security and correctness statements are not defended with the wrong implication.
Source Map
| Source | Use it for |
|---|---|
| MIT Mathematics for Computer Science | Proof structure, sets, induction, and discrete reasoning. |