[HD] EECS3342 F26 - 2026-10-22 (Thursday) - Lecture 11

Overview

EECS3342 Lecture 11 distinguishes safe states, defined by invariants, from enabled events, defined by guards, using a bridge-capacity model to show how guard design restricts reachable states. It introduces Event-B before-after predicates and sequent notation, then sketches invariant-preservation proof obligations by translating event actions such as ML out into post-state goals.

Key takeaways

A state is safe because it satisfies the invariant, while an event is enabled because its guard is true; these checks are logically separate.
A guard must prevent reachable unsafe states, but it may intentionally block transitions to states that would still satisfy the invariant.
In Event-B action notation, updates are simultaneous constraints: x becomes y and y becomes x translates to x′ = y ∧ y′ = x, not sequential assignments.
A sequent H ⊢ G means the conjunction of hypotheses H implies goal G; with no hypotheses, the goal must hold without additional assumptions.
To check ML out preserves n ≤ D, substitute its before-after predicate n′ = n + 1 into the post-state invariant, yielding n + 1 ≤ D; the precondition n ≤ D alone does not guarantee that goal.

Chapters

0:00 Written Test One, Sunday Zoom Review, and Lab Three

Written Test One is scheduled for Wednesday, October 28, with a reminder about critical rules to follow.
The programming test is still being graded, and Jackie Wang plans to follow up with the TA.
Students are asked to keep Lab Three on track; a Sunday Zoom review is planned for roughly 4:00 to 5:00 p.m., with the exact time to be confirmed.
A recorded walkthrough of the written-test practice questions is already on the lecture site, and Sunday’s Zoom can focus on follow-up questions.

2:30 Bridge Controller Review and the Role of Event Guards

The lecture continues the bridge-controller case study, building on the ML out and ML in events and the variable that tracks cars on the island and bridge.
A complete transition diagram is not required for this course; students should instead trace events when checking whether an invariant can be violated.
The lecture sets up a distinction between whether a state is safe and whether an event is enabled.

4:38 Safe States Depend on Invariants, Not Guards

A state is safe when it satisfies the invariant, such as n ≤ D for the bridge’s car capacity.
An event is enabled when its guard evaluates to true in the current state.
These are separate checks: the invariant defines safety, while the guard is part of the event’s design.

6:11 An n ≤ 1 Guard Restricts the ML Out Event

The example uses the invariant n ≤ D and gives ML out the guard n ≤ 1.
The event action is written n := n + 1, meaning n becomes its prior value plus one in the specification.
The guard is an enabling condition chosen by the model designer; the example uses the artificial limit of one to illustrate its effect.

9:19 Tracing Safe but Unreachable Bridge States

With D = 3 and initial n = 0, the state is safe and ML out is enabled because 0 ≤ 1.
After ML out, n = 1 remains safe and the event is still enabled; after another transition, n = 2 is also safe.
At n = 2 the guard n ≤ 1 disables ML out, even though a hypothetical further transition to n = 3 would still satisfy n ≤ 3.
A sound guard must not allow a transition to an unsafe state, but it need not make every mathematically safe state reachable.

18:17 Guard Design, Model Checking, and Theorem Proving

Whether a guard reaches all safe states depends on the application; a designer may intentionally impose stricter limits than capacity requires.
Model checking builds a complete transition graph and traverses it, for example with breadth-first search, to find unsafe states.
EECS3342 focuses on theorem proving rather than enumerating the complete graph; model checking is mentioned as background for a later course.

20:22 Before-After Predicates Give Event Actions Precise Meaning

A state transition has a pre-state and a post-state; an unprimed variable such as n denotes its pre-state value.
A primed variable such as n′ denotes the post-state value, so ML out is represented by the before-after predicate n′ = n + 1.
Constants do not change between states and therefore do not need pre-state or post-state prime notation.
The action syntax used in a Rodin-style model is a specification, which must be translated into a before-after predicate for mathematical verification.

28:25 Why Sequential Swap Assignments Fail as a Formal Specification

The apparent three-step swap using temp, x, and y would work as sequential Java assignments but not as a formal event action.
In the before-after interpretation, every right-hand-side variable refers to the pre-state, while each left-hand-side variable denotes its post-state value.
For pre-state x = 23, y = 46, and temp = −1, the three actions yield post-state temp = 23, x = 46, and y = −1, not a swap.

34:18 Specify a Swap with Parallel Event Constraints

The correct formal swap action is x becomes y and y becomes x, with both updates interpreted together.
Its before-after predicate is x′ = y ∧ y′ = x.
The assignments are parallel constraints, not sequential implementation steps; the post-state values come from the same pre-state.

37:07 Invariant Preservation as a Proof Obligation

Invariant preservation is formulated as a proof obligation, which will be written as a sequent.
The relevant state valuations satisfy the model’s typing constraints, and the desired property is that the invariant holds for the states under consideration.
To disprove a universal claim, provide a witness state that satisfies the relevant conditions but violates the invariant.
For this course, students prove obligations with inference rules rather than explicitly enumerating every valuation; exhaustive enumeration can face state explosion.

44:10 Sequent Syntax: Hypotheses Above the Turnstile, Goals Below

A sequent uses the turnstile symbol, written horizontally or vertically, with a set of hypotheses on the left or above and goals on the right or below.
Its meaning is that the conjunction of the hypotheses implies the goal or conclusion.
A sequent may be true or false; whether a goal follows from its hypotheses is assessed using inference rules.

50:57 Testing Sequent Validity and Interpreting No Hypotheses

The proposed goal n + 1 ≤ D does not follow from D ∈ ℕ, n ∈ ℕ, and n ≤ D; the counterexample n = D = 10 makes the goal false.
A sequent with no hypotheses is interpreted as true implying the goal, so the goal must be provable without extra assumptions.
Interpreting no hypotheses as false would make false imply any goal and would let every claim be proved automatically.

58:01 Sketching an Invariant-Preservation Sequent

A proof obligation for an event aims to show that the invariant holds in the post-state after the event executes.
The supporting hypotheses include model axioms, the invariant holding in the pre-state, and the event’s guard.
The sketch separates what can be assumed before the transition from the post-state invariant that must be proved.

1:00:21 ML Out Proof Obligation and Eliminating Post-State Primes

For ML out, the hypotheses include D ∈ ℕ, the pre-state conditions n ∈ ℕ and n ≤ D, and the event guard, which is true when no guard is specified.
The post-state invariant is first written using primes: n′ ∈ ℕ and n′ ≤ D.
Using ML out’s before-after predicate n′ = n + 1 eliminates the primes, producing the goal n + 1 ∈ ℕ and n + 1 ≤ D.
The pre-state and post-state formulas express the same invariant at different points in the transition; proving the post-state version is the preservation task.

Transcript excerpt

0:06 Okay. So, your written test one will be next Wednesday, uh, October 28th, right? During your enroll session, I'll send you guys a reminder just about the critical rules, but I'll be in touch. Your programming test is still being graded. I haven't heard back from the TA just yet, but I'll follow follow up with them. Maybe tomorrow, maybe around the afternoon. That's a deadline I gave to them. I'll follow up with them and I'll keep you guys posted. Should be on track. Uh, please work on lab three. Okay, just make sure it's on track. And then for written test, I want to show you guys one thing. So, as I confirmed, there will be a Zoom session this Sunday. Let me confirm the time with you. Uh, but most likely maybe around the uh late afternoon, early evening, maybe about 400 p.m. 5:00 pmish. I'll confirm. I'll send you guys a Zoom

0:53 invite as well. Okay. But I would suggest if you have any doubts about a practice question, I just posted this right before the class today. I'll show it to you. So we don't need to repeat the efforts in the actual zoom session. Right. So if you go to lecture site, you will see that let me refresh it. Okay. You will see the on the lecture site. Sorry, just a bit slow for my browser. Okay, there we go. All right. So you will see that under uh right be right underneath about the guide to written test one this is something new right it's about written test one practice question solution walkth through this is a session I did about one year or two years ago that one there goes through exactly the set of practice question I

1:41 gave to you guys on e-class so if you

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.