[HD] EECS3342 F26 - 2026-10-27 (Tuesday) - Lecture 12

Overview

Jackie Wang explains Event-B invariant-preservation proof obligations, showing how to substitute an event’s before-after predicate into a post-state invariant using a bank-withdrawal example. The lecture formalizes proof-obligation components, shows that two events and two invariants generate four preservation sequences, and introduces inference rules as a distinct way to reduce proof goals.

Key takeaways

Invariant preservation in Event-B is a transition-level obligation: assume the pre-state invariant and an event’s guard, then prove the invariant with state variables evaluated in the post-state.
For the bank withdrawal event, the post-state balance is B overridden at account A with B(A) − V; proving the invariant therefore requires checking the modified function, not merely replacing a scalar with a new value.
Constants and quantified dummy variables are not primed during post-state substitution; only state variables change between pre-state and post-state.
With two events and two invariants, Event-B generates four invariant-preservation sequences; adding one invariant adds one obligation per event, while adding one event adds one per invariant.
Changing an existing event’s guard does not inherently add obligations, but all preservation proofs for that event must be revisited because their provability may change.
An inference rule has a set of antecedent sequences and one consequent sequence; proving the antecedent is sufficient to establish the consequent, while an empty antecedent makes the consequent an axiom.

Chapters

0:00 Written Test 1 Logistics and Upcoming Course Work

Attend only the lab session in which you are enrolled for Written Test 1.
Bring blank sketch paper and a mobile phone for Duo Mobile verification.
Test your ECS login and Passport York access before the test; lab monitors cannot provide extra time for login fixes.
Lab 3 is due next Wednesday, and Lab 4 will be the final lab; the exam date and one-page data-sheet guidance are still forthcoming.

2:10 Sequent Notation and the Difference from Inference Rules

A sequent represents a proof obligation, often written horizontally or vertically, and is not automatically provable.
The lecture previews inference rules as a related but distinct concept that will explain how proof steps are justified.
For invariant preservation, begin with primed post-state variables and use the event’s before-after predicate to replace them.

3:45 Bank Withdrawal Model: Balance Invariant and Event

The bank model uses balance function B from accounts to integers and assumes constant C.
Its invariant requires every account x in dom(B) to satisfy B(x) ≥ −C.
The withdraw event takes account A and natural-number amount V, requires A ∈ dom(B), and updates B by overriding A’s balance with B(A) − V.
The account-membership guard alone may not protect the invariant if the withdrawal amount is too large.

9:30 Building the Invariant-Preservation Sequent

Treat withdrawal as a transition from a pre-state to a post-state.
The preservation sequent assumes the model axioms, the event guard A ∈ dom(B), and the unprimed invariant.
The goal is the same invariant evaluated in the post-state, represented by priming state variables.

13:00 Substituting the Overridden Balance into the Post-State Invariant

For the quantified invariant, prime the state variable B but leave constant C and dummy quantified variable X unprimed.
The withdraw before-after predicate gives B′ = B overridden at A with B(A) − V.
Substituting that function into the goal asks whether every account in the modified balance function still has a balance at least −C.
Rodin can reason that A remains in the domain, but the changed balance may require additional proof about the withdrawal amount.

20:45 Sequents: Hypothesis Order and Formal Proof Components

Sequent hypotheses are implicitly conjoined, so their order does not affect logical validity.
Organize hypotheses clearly because their order serves as documentation and inference rules can rearrange them during proof.
Formal Event-B proof obligations refer to named groups such as axioms, invariants, variables, guards, and event effects.

23:00 Event-B Constants, Axioms, Variables, and Invariant Labels

In the M0 example, the constant list contains d, and the axiom list refers to labels rather than rewriting each axiom’s formula.
The variable list contains n in the pre-state and n′ in the post-state.
Invariant lists can refer to all invariants together as I or to one indexed invariant, such as I₁.
An invariant may depend on both constants and state variables.

31:00 Guards, Effects, and Before-After Predicates

Each event has its own guard, which may depend on constants and variables; an event with no explicit guard has guard true.
Effects record the right-hand-side values assigned to post-state variables, such as n + 1 for ML_out and n − 1 for ML_in.
A before-after predicate equates each post-state variable with its corresponding effect, for example n′ = n + 1.
For a two-variable swap, effects are the ordered pair (Y, X), yielding X′ = Y and Y′ = X.

40:00 Counting Invariant-Preservation Obligations

The M0 proof obligation considers each event guard separately and proves each indexed invariant separately.
With events ML_out and ML_in and invariants I₁ and I₂, the required count is 2 × 2 = 4 sequences.
The post-state invariant goal is formed by applying the event’s effects to one invariant at a time.

46:30 Naming Proof Obligations and Extending the Model

Proof-obligation names identify the event, invariant index, and purpose, such as ML_out / invariant 01 / invariant preservation.
Adding invariant I₃ to a model with two events adds two preservation obligations, one for each event.
Adding a new event E when three invariants exist adds three obligations, one for each event-invariant pair.
Rodin automates generation, but developers should understand how model changes affect the obligation set.

54:10 Guard Changes Require Rechecking Existing Proofs

Changing an event guard does not create a new event-invariant pair, so it does not necessarily add new obligations.
Existing obligations for that event must be revisited because strengthening or weakening its guard can change whether they remain provable.
Even replacing a guard with true requires checking the event’s previously generated preservation obligations.
Possible exam tasks include naming all invariant-preservation obligations or writing one or more complete sequents.

1:00:10 Inference-Rule Syntax: Antecedents, Consequents, and Labels

An inference rule is written vertically with an antecedent A, a consequent C, and a label L naming the rule.
A is a set of sequences, while C is a single sequence; these are sequences rather than bare predicates.
The rule expresses that proving the antecedent sequences is sufficient to prove the consequent sequence.
Compare this notation with the sequent notation from slide 16 to avoid treating the two concepts as interchangeable.

1:05:00 Inference-Rule Semantics and Proof Direction

An inference rule is assumed as a valid proof step rather than something that must be proved each time it is applied.
Its semantic justification reduces to the antecedent conditions implying the consequent, consistent with sequences representing implications.
The direction matters: to prove C, it is sufficient to prove A, not the reverse.

1:08:00 Empty Antecedents, Axioms, and Review Before Thursday

A rule with no antecedent requires proving only true, so its consequent C can be accepted as an axiom.
This means C itself is assumed without proof, which differs from assuming an implication A ⇒ C.
Before Thursday, review slides 16, 18, and 20, focusing on sequents, formal proof-obligation components, and inference rules.

Transcript excerpt

0:05 Okay, so your written test number one tomorrow, uh, make sure you only go to your your enroll lab session. Okay, so please double check before you go. And for tomorrow, let me see. Uh, you got your guide and also example questions on the lecture site. This also post a video to go over each question with you just in case you need it. Uh, please bring your own sketch paper. Make sure it's blank on both sides. We don't really have enough sketch paper for you, right? We just didn't prepare for that. So, please make sure you bring your own. And tomorrow, you will need your mobile phone. Please make sure you have it. You're going to need that for your do mobile verification. And also, if you haven't already tested yet, so please do so. We cannot really give you any extra time for anytime you have to ask a lab monitor to fix your ECS login and also passport York. Right? So, these two are

0:53 both required for tomorrow. And if you have haven't tested, maybe just do that quickly after class, right? I think the lab are still open. Uh your lab three, I believe you will be due uh next Wednesday. So just make sure it's still keep track of it. And then we I'm going to release your lab number four also in time. That'll be the final lab for the semester. Okay. Uh everything's in place, lecture digest and notes template, etc. Okay. I don't know the exam day just yet. So once I know about it, we can maybe start talking about the exam. Okay. I'll definitely give you guys maybe some guidance and also about the data sheets that you have to put together. You're allowed to bring one.

This is the start of the transcript. Save this video free for the whole transcript, searchable and time-coded.

Related notes

Summary, takeaways, and chapters were generated by AI from the video's transcript and may contain errors. The video belongs to its creator, Jackie Wang.