Sharper questions with assertions
Once the covers look right, write down the designer's assumptions about the design as assertions. For the lift these are the safety properties in the wrapper:
| Assertion | Designer's intuition | Expected |
|---|---|---|
a_door_not_moving | Never move with the door open | proven (the FSM encodes it) |
a_no_wrap | Never try to go above floor 3 or below floor 0 | proven |
a_one_floor | Each MOVE changes the floor by exactly one in the travel direction | proven |
a_open_for_call | The door only opens for a call | proven |
a_clear_served | A call is only forgotten when that floor is served | proven |
a_no_wrap is a nice example of formal checking something a designer "knows" is impossible. The 2-bit
floor + 1 would silently wrap from 3 to 0 — but the controller only moves up when there is a call
above it. The proof confirms that reasoning for every possible sequence of button presses.