Your .md File Is Not a Specification: Using Formal Analysis to Find Requirements Gaps

Let us say we want to build a small appointment booking app for a salon. A product manager might write,Build a salon appointment booking app where customers can book appointments with stylists. Stylists must be able to set their own schedules, and all appointments must be within their schedule.Here, the requirements look simple. For a real application, there are many unanswered questions (like how many stylists, who manages the stylists and so on) and a full requirements document might span multiple pages. For now, let us focus on these two lines alone as stated.  Are there any ambiguities? Are they consistent? Are they complete? Are they testable? And more importantly, if we give them to a software engineer or a coding agent, will it build what we actually want?To reduce ambiguity in requirements wording, many organizations use the Easy Approach to Requirements Syntax (EARS) notation. For example, the above requirements become,R1: THE SYSTEM SHALL allow the stylist to set their work schedule. R2: THE SYSTEM SHALL allow a customer to book an appointment with the stylist. R3: THE SYSTEM SHALL ensure that all appointments are within the stylist's schedule.At first glance this set of requirements might seem well specified. But the requirement R3 is not directly testable. It describes a property, constraints and data invariants that must hold across states, rather than an observable behavior we can test with a test case. Invariants cannot be tested. You can only test for preconditions and postconditions. Invariants must be reasoned about from these testable pre- and post- conditions.To make it testable, we need to describe the behaviors that establish this property. For example, what should happen when a customer requests a slot within the stylist's schedule? What should happen when they request a slot outside it?In this article, we will see how to make requirements complete, unambiguous, consistent, and testable.To do that, we need a way to describe not only the properties we want the system to satisfy, but also how those properties relate to the actions that change the system. Dynamic Logic, also known as the Logic of Actions, provides a way to express these relationships.Formal modeling with Dynamic LogicDynamic Logic is a formal approach to reasoning about what actions or operations can happen and how they affect the state.A short tutorial on Dynamic LogicDynamic logic introduces two notations. [A]p: p holds after every possible execution of A. e.g. [Rain]GroundIsWet<A>p: A can happen, and p holds after at least one execution of it.  e.g. <SunShine>GroundIsDryThat is, if it rains, the ground will get wet. But when the sun shines, the ground might dry out.Often, an action has a precondition that must hold before it can produce a particular result: PreCondition → [Action]PostCondition For example: RoomIsDark -> [ToggleSwitch] RoomIsLitRoomIsLit -> [ToggleSwitch] RoomIsDark For practical applications, we often specify an initial state before any modeled actions occur. For example, mark the dark state as the initial state. We could also use variables instead,init: room="dark" room="dark" -> [ToggleSwitch] room="lit" room="lit" -> [ToggleSwitch] room="dark" If action A is disabled, [A]p vacuously holds irrespective of p, whereas <A>p is false irrespective of p. That is, with the above example, if there is no switch at all to toggle, then both the statements hold.To require that A is enabled, add <A>True. To require that it is blocked, add [A]False.init: room="dark" room="dark" -> [ToggleSwitch] room="lit" room="lit" -> [ToggleSwitch] room="dark" <ToggleSwitch> TrueAt this point, we could model our salon appointment system. Modeling salon appointment booking systemLet's model a simplified version of the requirements: a single stylist, a single customer, and a single time slot.init: ¬scheduled_to_work # read it as `not scheduled to work` ¬appointment_booked # R1: <set_schedule> scheduled_to_work <set_schedule> ¬scheduled_to_work # R2: <book_appointment> True [book_appointment] appointment_booked # R3: appointment_booked → scheduled_to_work💡In a pure mathematical model, stating what an action changes isn't enough; we must also state what it leaves unchanged. [book_appointment] appointment_booked says nothing about scheduled_to_work, so we'd need separate frame axioms such as scheduled_to_work → [book_appointment] scheduled_to_work (and its negation). The model above omits these for brevity. With many variables and actions, these axioms multiply quickly; this is known as the frame problem.FizzBee, which we'll use next, sidesteps this the way most programming languages do: any variable an action doesn't assign keeps its value.Note: appointment_booked → scheduled_to_work is a standard propositional logic expression, there is no action here. That is, if the appointment is booked then the stylist must be scheduled to work. This is usually expressed as not appointment_booked or scheduled_to_work in standard programming languages like Python.Note: This is a simplified model for pedagogical purposes. FizzBee.ai can generate a much more detailed specification, including roles such as Customer and Stylist, multiple time slots, and explicit definitions of who can perform each action.Verification with FizzBeeLet us convert the above model into FizzBee specification language.Open in FizzBee Playgroundaction Init: scheduled_to_work = False appointment_booked = False # R1 atomic action SetSchedule: scheduled_to_work = oneof [False, True] # R2 atomic action BookAppointment: appointment_booked = True # R3 always assertion BookingsInSchedule: return not appointment_booked or scheduled_to_workYou can run this spec directly in the FizzBee online playground or install and run FizzBee locally. Each FizzBee snippet in this tutorial includes an Open in FizzBee Playground link above the code that opens the spec with the code pre-filled.When you run it, you will see a trace like this. FAILED: Model checker failed. Invariant:  BookingsInSchedule------Init--state: {"appointment_booked":false,"scheduled_to_work":false}------BookAppointment--state: {"appointment_booked":true,"scheduled_to_work":false}------ This error is obvious. We did not add a precondition to check if the stylist is scheduled to work before booking the appointment.This changes R2.# R2: scheduled_to_work → <book_appointment> True scheduled_to_work → [book_appointment] appointment_booked # R2b: ¬scheduled_to_work → [book_appointment] FalseIn EARS, R2 becomes more specific, and we add R2b to handle the rejection case.R1: THE SYSTEM SHALL allow the stylist to set their work schedule. R2: WHEN a customer requests a slot within the stylist's work schedule, THE SYSTEM SHALL book the appointment. R2b: IF a customer requests a slot that is not within the stylist's work schedule, THEN THE SYSTEM SHALL reject the request. R3: THE SYSTEM SHALL ensure that all appointments are within the stylist's schedule.Review the requirements again. Do you see any issues? R3 appears to be a direct implication of R2 and R2b. Before we change much, let us check with FizzBee.Open in FizzBee Playground# R2 atomic action BookAppointment: require scheduled_to_work # <---- Add this precondition appointment_booked = TrueWhen you run it again in the playground, you will see a longer trace, FAILED: Model checker failed. Invariant:  BookingsInSchedule------Init--state: {"appointment_booked":false,"scheduled_to_work":false}------SetSchedule--state: {"appointment_booked":false,"scheduled_to_work":false}------Any:scheduled_to_work=True--state: {"appointment_booked":false,"scheduled_to_work":true}------BookAppointment--state: {"appointment_booked":true,"scheduled_to_work":true}------SetSchedule--state: {"appointment_booked":true,"scheduled_to_work":true}------Any:scheduled_to_work=False--state: {"appointment_booked":true,"scheduled_to_work":false}------ This is a less obvious error. What this error shows is that if the stylist marks themselves as not working after an appointment is booked, the old appointment still remains in the system.The Missing RequirementThe issue FizzBee found is,Stylist sets their schedule as 9am - 5pmCustomer books the 9am slotThe stylist changes their schedule to 10am -  6pm. What should happen to the 9am appointment?Option 1: Block update on conflictDo not let the stylist change the schedule if there is already a booking.# R1 atomic action SetSchedule: require not appointment_booked # <--- Precondition scheduled_to_work = oneof [False, True]This will fix the issue. However, from a product perspective, if a stylist wants to call in sick, the system prevents them from updating their schedule. In most cases, the stylist would not show up and the customer will be unhappy.Option 2: Cascade cancelAutomatically cancel the appointment.atomic action SetSchedule: scheduled_to_work = oneof [False, True]