Proofs and Discrete Structures: Case Studies

These are constructed teaching cases. Their guarantees apply to the explicit models below; deployment introduces additional assumptions to verify.

Case 1: Sequential admission counter

A toy fixed-window counter starts at c=0 with integer limit L≥0. A request is accepted exactly when c<L; an accepted request increments c, a rejected request leaves c unchanged. A reset begins a new window at zero. Operations are atomic and sequential, with exact arithmetic. Prove 0≤c≤L by induction on operations. Then count accepted requests since the last reset and relate that count to c.

Stress point: with L=1, two concurrent requests can both read c=0 and accept before either updates it. The sequential proof's atomic-operation assumption fails. Submit the proof and that interleaving; do not claim a production rate limiter from this counter alone. A sliding window is a different model.

Case 2: Grant and deny sets

Fix universe U={read,write,export}. A toy policy declares effective permissions to be (role grants ∪ direct grants) ∖ explicit denies. With role={read,write}, direct={export}, deny={write}, the result is {read,export}. Absence of a direct grant is not an explicit deny. Precedence is part of this chosen specification.

Stress point: compare a second rule where direct grants override denies. Give the same user's results under both rules. Submit the set definitions and a membership proof for one operation. Set algebra cannot choose a business policy; it makes the selected policy precise enough to examine.

Case 3: Representative-dependent workflow labels

Two states can reach each other, so the analyzer groups them in one class. One state is labeled “queued” and the other “checked.” Reporting the first member's label makes the class label change when iteration order changes.

Stress point: demonstrate that equal class inputs yield inconsistent proposed outputs. A valid repair is a label constant on each class, or a class label that explicitly stores the set of member labels. These express different requirements. Submit the representative-independence proof and connect it to the workflow capstone.