Chapter 1 — Mathematical reasoning
Lesson map
Lesson 01 published. Map, example, EX001.
flowchart TD
N0["Learning outcomes"]
N1["1.1 The case"]
N2["1.2 Precise rules"]
N3["1.3 Implication and negation"]
N4["1.4 Gaps and contradictions"]
N5["1.5 Quantifiers"]
N6["Synthesis"]
N0 --> N1 --> N2 --> N3 --> N4 --> N5 --> N6
N6 --> EX["Worked example"]
EX --> Q["Exercise EX001"]
Logical drawing
flowchart LR
N0["Learning outcomes"]
N1["1.1 The case"]
N2["1.2 Precise rules"]
N3["1.3 Implication and negation"]
N4["1.4 Gaps and contradictions"]
N5["1.5 Quantifiers"]
N6["Synthesis"]
N0 --> N1 --> N2 --> N3 --> N4 --> N5 --> N6 --> Q["EX001"]
[Learning outcomes]
|
v
[1.1 The case]
|
v
[1.2 Precise rules]
|
v
[1.3 Implication and negation]
|
v
[1.4 Gaps and contradictions]
|
v
[1.5 Quantifiers]
|
v
[Synthesis]
|
v
[Worked example] --> [Exercise EX001]
Learning outcomes
You will (1) use logical statements to express security rules precisely; (2) reason with implication and negation; (3) check rules for contradictions and gaps; (4) introduce the course case.
1.1 The case
Lena Fischer is a computer science student at the fictional Hollowbrook University. She joins the student developer society that runs CampusEats, a web app for ordering food from campus cafés, and is mentored by Grace Nwosu, the university's application security lead. In her first month, a CampusEats developer accidentally pushed a payment-provider token to the project's public repository; a scanner flagged it two hours later and the token was revoked. The same week, the build stopped because a downloaded package did not match its recorded hash. These two events, a leaked secret and a supply-chain integrity check, start Lena's four-year journey.
1.2 Precise rules
Security rules are logical statements. "Only staff may change menu prices" can be written: if a user changes a price, then the user is staff. Writing rules this way exposes ambiguity: does "staff" include student volunteers who run the café till? CampusEats decides they are a separate role, "volunteer", without price rights.
Each rule in the CampusEats design notes is now written in this if-then form, with every role named. Ambiguous words such as "staff" are defined once in a glossary, so developers, café managers and reviewers read the rule the same way and tests can be written directly from it.
1.3 Implication and negation
The contrapositive of "if price change then staff" is "if not staff then no price change". Tests check the contrapositive: a volunteer tries a price change and must be refused. Negating a rule correctly matters: the opposite of "all requests are logged" is "some request is not logged", not "no requests are logged".
Lena writes one refusal test for each rule, and a careful negation for each logging claim, so that a single missing log entry is enough to fail the check.
1.4 Gaps and contradictions
Two rules "volunteers may issue refunds up to £5" and "only staff may issue refunds" contradict each other. Lena's table of roles and actions makes such conflicts visible before code is written.
The table has roles as rows and actions as columns, and each cell says allowed, refused or undecided. Undecided cells are gaps: nobody has said what should happen. Contradictions show up as two rules putting different answers in the same cell. The society resolves the refund conflict by letting volunteers refund up to the small limit and requiring staff for anything larger, then rewrites both rules so they agree.
1.5 Quantifiers
"Every dependency has an owner" is a universal statement; one counterexample disproves it. Lena checks the CampusEats dependency list and finds three packages with no named owner.
An existential statement works the other way: "some package is unmaintained" is proved by one example. Lena's finding turns the universal rule into a task list. Each of the three packages is either given a named owner from the society or scheduled for removal, and the rule is rechecked after each change so that the statement "every dependency has an owner" is true again before the next release.
Worked example
Lena writes CampusEats' access rules as eight logical statements and a role–action table. She finds the refund contradiction and two actions (export orders, edit opening hours) with no rule at all. The society's lead developer resolves them in a short meeting.
Synthetic case. Hollowbrook University, CampusEats, its people and all events are synthetic.
Errors and limits
Logic makes rules precise but cannot decide what the right business rule is; people must.
Exercises
- EX001 — Contrapositive. Give the contrapositive of "if a user changes a price, the user is staff". Rubric: 3 = if not staff then no price change; 2 = partial; 1 = vague; 0 = none.
- EX002 — Negation. Negate "all requests are logged". Rubric: 3 = some request is not logged; 2 = partial; 1 = wrong; 0 = none.
- EX003 — Contradiction. What contradiction did Lena find? Rubric: 3 = volunteer refunds up to £5 vs only staff refunds; 2 = partial; 1 = vague; 0 = none.
Synthesis
Precise logical rules expose gaps and contradictions before they become flaws.