.md 文件不是规格说明：用形式化分析找出需求缺口

假设我们想为一家沙龙构建一个小型预约预订应用。产品经理可能会这样写：

构建一个沙龙预约预订应用，客户可以预约造型师。造型师必须能够设置自己的日程安排，并且所有预约都必须在其日程安排之内。

在这里，需求看起来很简单。对于真实的应用来说，还有许多未解答的问题（比如有多少造型师、谁管理造型师等等），完整的需求文档可能会长达数页。现在，让我们仅按所述内容关注这两行。是否存在任何歧义？它们是否一致？是否完整？是否可测试？更重要的是，如果我们把它们交给软件工程师或编码代理，它会构建出我们真正想要的东西吗？

为了减少需求措辞中的歧义，许多组织使用需求语法简易方法（EARS）表示法。例如，上述需求变为，

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.

乍一看，这组需求似乎定义得很好。但需求 R3 不能直接测试。它描述的是一个属性、约束和数据不变量，这些必须在各个状态之间保持成立，而不是我们可以用测试用例来测试的可观察行为。

不变量无法被测试。你只能测试前置条件和后置条件。不变量必须从这些可测试的前置条件和后置条件中推理得出。

为了使其可测试，我们需要描述建立该属性的行为。例如，当客户请求造型师日程安排内的一个时段时应该发生什么？当他们请求日程安排之外的一个时段时应该发生什么？

在本文中，我们将了解如何使需求完整、无歧义、一致且可测试。

为此，我们需要一种方式，不仅能描述我们希望系统满足的属性，还能描述这些属性与改变系统的动作之间的关系。动态逻辑，也称为动作逻辑，提供了一种表达这些关系的方式。

使用动态逻辑进行形式化建模

动态逻辑是一种形式化方法，用于推理可能发生哪些动作或操作，以及它们如何影响状态。

动态逻辑简短教程

动态逻辑引入了两种记号。

[A]p：在 A 的每一种可能执行之后，p 都成立。
例如 [Rain]GroundIsWet

<A>p：A 可以发生，并且在它的至少一次执行之后 p 成立。
例如 <SunShine>GroundIsDry

也就是说，如果下雨，地面会变湿。但当阳光照耀时，地面可能会变干。

通常，一个动作有一个前置条件，在它能够产生特定结果之前必须成立：

PreCondition → [Action]PostCondition

例如：

RoomIsDark -> [ToggleSwitch] RoomIsLit

RoomIsLit -> [ToggleSwitch] RoomIsDark

对于实际应用，我们通常在任何建模动作发生之前指定一个初始状态。例如，将黑暗状态标记为初始状态。

我们也可以改用变量，

init: room="dark"

room="dark" -> [ToggleSwitch] room="lit"
room="lit"  -> [ToggleSwitch] room="dark"

如果动作 A 被禁用，则无论 p 是什么，[A]p 都空洞地成立，而无论 p 是什么，<A>p 都为假。也就是说，在上面的例子中，如果根本没有开关可供切换，那么这两个陈述都成立。
要要求 A 被启用，添加 <A>True。要要求它被阻止，添加 [A]False。

init: room="dark"

room="dark" -> [ToggleSwitch] room="lit"
room="lit"  -> [ToggleSwitch] room="dark"
<ToggleSwitch> True

此时，我们可以对沙龙预约系统进行建模。

对沙龙预约预订系统进行建模

让我们对需求的一个简化版本进行建模：单个造型师、单个顾客和单个时间段。

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

💡

在纯数学模型中，仅说明一个动作改变了什么是不够的；我们还必须说明它保持不变的内容。[book_appointment] appointment_booked 没有提及 scheduled_to_work，因此我们需要单独的框架公理，例如 scheduled_to_work → [book_appointment] scheduled_to_work（及其否定）。为简洁起见，上述模型省略了这些。当变量和动作很多时，这些公理会迅速增多；这被称为框架问题。
我们接下来要使用的 FizzBee 像大多数编程语言一样绕过了这个问题：动作未赋值的任何变量都保持其值。

注意：appointment_booked → scheduled_to_work 是标准命题逻辑表达式，这里没有动作。也就是说，如果预约已预订，那么造型师必须被安排工作。在 Python 等标准编程语言中，这通常表示为 not appointment_booked or scheduled_to_work。

注意：这是出于教学目的的简化模型。FizzBee.ai 可以生成更详细的规范，包括 Customer 和 Stylist 等角色、多个时间段，以及每个动作可由谁执行的明确定义。

使用 FizzBee 进行验证

让我们将上述模型转换为 FizzBee 规范语言。

在 FizzBee Playground 中打开

action 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_work

你可以直接在 FizzBee 在线 playground 中运行此规范，或者在本地安装并运行 FizzBee。本教程中的每个 FizzBee 代码片段都在代码上方包含一个 Open in FizzBee Playground 链接，点击后会打开预填代码的规范。

运行它时，你会看到如下跟踪。

FAILED: Model checker failed. Invariant: BookingsInSchedule
------
Init
--
state: {"appointment_booked":false,"scheduled_to_work":false}
------
BookAppointment
--
state: {"appointment_booked":true,"scheduled_to_work":false}
------

这个错误很明显。我们没有添加前置条件来检查在预订预约之前造型师是否被安排工作。

这改变了 R2。

# R2:
scheduled_to_work → <book_appointment> True
scheduled_to_work → [book_appointment] appointment_booked

# R2b:
¬scheduled_to_work → [book_appointment] False

在 EARS 中，R2 变得更加具体，并且我们添加 R2b 来处理拒绝情况。

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.

再次审查需求。你发现任何问题了吗？R3 似乎是 R2 和 R2b 的直接推论。

在我们做太多更改之前，让我们用 FizzBee 检查一下。

在 FizzBee Playground 中打开

# R2
atomic action BookAppointment:
    require scheduled_to_work    # <---- Add this precondition
    appointment_booked = True

当你再次在 playground 中运行它时，你会看到更长的跟踪，

失败：模型检查器失败。不变式： 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}
------

这是一个不太明显的错误。这个错误表明，如果造型师在预约被预订后将自己标记为不工作，旧预约仍然留在系统中。

缺失的需求

FizzBee 发现的问题是，

造型师将自己的日程设置为上午 9 点至下午 5 点
客户预订了上午 9 点的时段
造型师将日程改为上午 10 点至下午 6 点。

上午 9 点的预约应该如何处理？

选项 1：冲突时阻止更新

如果已有预约，则不允许造型师更改日程。

# R1
atomic action SetSchedule:
    require not appointment_booked  # <--- Precondition
    scheduled_to_work = oneof [False, True]

这会修复该问题。然而，从产品角度来看，如果造型师想请病假，系统会阻止他们更新日程。在大多数情况下，造型师不会出现，客户会不满意。

选项 2：级联取消

自动取消预约。

atomic action SetSchedule:
    scheduled_to_work = oneof [False, True]
    appointment_booked = appointment_booked and scheduled_to_work  # <-- Cancel the appointment

这也能解决不变式违规，但可能导致糟糕的用户体验。当造型师请病假时静默取消预约，很少是店主想要的结果。

选项 3：允许更改并显式处理受影响的预约

让日程更改通过，并将这些例外标记出来，供沙龙经理（可能在联系客户后）重新安排到不同的造型师或不同的时间。

此选项可能仅适用于多造型师的沙龙，并引入了新的参与者和用例。这是产品负责人应做出的产品决策。将需求形式化有助于及早发现这些缺口。

到目前为止，我们有意简化了模型。形式化模型捕获了重要的状态和不变式，但丢失了原始需求中的一些信息：每个动作由谁执行。

对参与者和用例建模

让我们回到形式化的 FizzBee 模型。这是我们目前拥有的规范。
为简单起见，让我们选择选项 2（级联取消），在更新日程时自动移除冲突的预约。

在 FizzBee Playground 中打开

action Init:
    scheduled_to_work = False
    appointment_booked = False

# R1
atomic action SetSchedule:
    scheduled_to_work = oneof [False, True]
    appointment_booked = appointment_booked and scheduled_to_work

# R2
atomic action BookAppointment:
    require scheduled_to_work
    appointment_booked = True

# R3
always assertion BookingsInSchedule:        
    return not appointment_booked or scheduled_to_work

在这里，我们还没有对参与者或用例建模。谁设置日程？谁预订预约？FizzBee 通过角色定义支持面向对象建模。

role Stylist:
    atomic action SetSchedule:
        scheduled_to_work = oneof [False, True]
        system.set_schedule(scheduled_to_work)

role Customer:
    atomic action BookAppointment:
        system.book()

作为需求分析的约定，我们使用角色 System 来表示系统本身。

role System:
    action Init:
        self.scheduled_to_work = False
        self.appointment_booked = False

    atomic func set_schedule(working):
        self.scheduled_to_work = working
        self.appointment_booked = self.appointment_booked and self.scheduled_to_work

    atomic func book():
        require self.scheduled_to_work
        self.appointment_booked = True

现在 init 动作和断言变为：

action Init:
    system = System()
    stylist = Stylist()
    customer = Customer()

always assertion BookingsInSchedule:
    return not system.appointment_booked or system.scheduled_to_work

你可以在 FizzBee playground 中运行它。

你还可以使用状态图和序列图以交互方式探索状态变化。在后续文章中，我们将展示如何对 UI 行为进行形式化建模并生成交互式原型。

定义多个 actor 实例

让我们再添加一个需求。允许客户取消他们的预约。如果你用 EARS 格式来写，它会是这样的。

R4：当客户请求取消自己的预约时，
系统应取消它。

R4b：如果客户请求取消一个不属于他们的预约，
那么系统应拒绝该取消请求。

为此，我们需要多个 customer 实例。按如下方式修改 Init 动作。（标准类 Python 代码）

action Init:
    system = System()
    stylist = Stylist()
    customers = []
    for _ in range(2):
        customers.append(Customer())

每个角色实例都有一个 __id__ 字段，客户应在请求中包含它。

role Customer:
    atomic action BookAppointment:
        system.book(self.__id__)

为了记录是谁进行了预约，我们可以修改 appointment_booked 来存储客户的 ID，或者在没有预约时存储 None。

因此，完整规范变为，

在 FizzBee Playground 中打开

role Stylist:
    atomic action SetSchedule:
        scheduled_to_work = oneof [False, True]
        system.set_schedule(scheduled_to_work)

role Customer:
    atomic action BookAppointment:
        system.book(self.__id__)

    atomic action CancelAppointment:
        system.cancel(self.__id__)

role System:
    action Init:
        self.scheduled_to_work = False
        self.appointment_booked = None

    atomic func set_schedule(working):
        self.scheduled_to_work = working
        if self.appointment_booked and not self.scheduled_to_work:
            self.appointment_booked = None

    atomic func book(customer_id):
        require self.scheduled_to_work
        # A precondition is underspecified
        self.appointment_booked = customer_id

    atomic func cancel(customer_id):
        require self.appointment_booked == customer_id
        self.appointment_booked = None

action Init:
    system = System()
    stylist = Stylist()
    customers = []
    for _ in range(2):
        customers.append(Customer())   

always assertion BookingsInSchedule:
    return not system.appointment_booked or system.scheduled_to_work

在 playground 中运行它，它会通过（有 4 个唯一状态）。

scheduled_to_work	appointment_booked
False	None
True	None
True	Customer0
True	Customer1

请注意，仍然存在一个未指定的行为，我们的形式化断言没有捕获到。这是一个重要的提醒：形式化方法不会自动发现每一个 bug。结果的好坏取决于我们指定的属性和断言。

💡

形式化方法并不是捕获所有 bug 的魔法解决方案。它们的好坏取决于你指定的属性或断言。

作为可执行规范的形式化规范

我们已经用于模型检查的规范也可以作为系统的交互式模型。利益相关者不必将需求作为静态文档来阅读，而是可以探索可能的行为并查看由此产生的状态变化。

这使得工程师、产品经理和其他利益相关者能够与规范进行交互，并发现它是否符合他们预期的行为。

在 playground 上，启用白板并再次运行模型检查器。它应该会创建另一个链接 'Explore'。点击它。

初始状态出现在右侧。

在左侧，你会看到可用的动作。点击 Stylist#0.SetSchedule。

选择 true。

状态变为

现在点击按钮为 Customer#0 预约。

现在状态显示已预约的预约。

但在左侧，你仍然会看到允许任一客户预约的按钮。

点击它。你会看到状态发生变化，Customer#0 的预约被 Customer#1 覆盖。

拥有可执行规范有助于我们模拟和探索所指定的行为，从而易于可视化和审查规范是否捕获了预期行为。

在这里，我们看到行为以类似白板的图表形式可视化。FizzBee.ai 可以更进一步，生成交互式 UX 原型，让非技术利益相关者也能探索行为。

修复：拒绝覆盖预约

修复很简单。在 EARS 格式中，

R2c：如果客户请求一个已被预约的时段，那么系统应拒绝该请求。

在 FizzBee 中，

    atomic func book(customer_id):
        require self.scheduled_to_work
        require not self.appointment_booked  # <-- R2c
        self.appointment_booked = customer_id

可选地，你可以像这样包含一个转换断言，它会在无效的状态转换上失败。

在 FizzBee Playground 中打开

transition assertion NoOverwritingAppointment(before, after):
    return ((not before.system.appointment_booked)
            or (not after.system.appointment_booked)
            or (before.system.appointment_booked == after.system.appointment_booked))

测试

由于我们现在有了可执行规范，能够生成完整的状态转换图，我们就可以广泛且自动地测试实现，而无需显式枚举测试用例。

基于模型的测试一次执行一个转换。通过从 Init 重放一条路径，将实现置于状态 S_i（映射到其规范状态），执行动作 A，然后检查：

如果 A 成功并到达 Sj，规范必须允许它：S_i → <A>S_j。
如果 A 失败，规范必须禁用它：S_i → [A] False。

第二条规则很重要：一个拒绝一切的实现仅凭第一条规则就能通过。

💡

精化与互模拟
规则 1 在形式化方法术语中给出了精化。精化确定具体系统 B 是否表现出抽象系统 A 的行为的子集。仅这一点对许多系统来说太弱了，因为一个拒绝每个动作的实现也能通过。
规则 2 弥补了这一差距。对于像本文中这样的确定性规范，这两条规则相当于互模拟。
当规范有意允许多个结果时，它们给出的是非阻塞精化，这通常是你想要的，因为实现可以合理地选择其中一个结果。

注意，我们从不在实现上断言不变式。那将是多余的，因为每个规范状态已经满足它，并且符合规范的转换会让我们保持在规范状态中。那也会太弱：block-on-conflict 和 cascade-cancel 都保持 BookingsInSchedule，但只有一个符合我们的需求。

通过这些测试可以增强信心，表明实现在所测试的行为上符合模型，但并不能证明在所有可能行为上都符合。

使用 FizzBee 进行基于模型的测试

FizzBee 附带了对多种语言的基于模型的测试支持，包括 Go、Java、Rust 和 TypeScript（包括使用 Playwright 进行浏览器测试，以及使用 Node.js 进行独立应用测试）。更多示例，你可以查看 https://github.com/fizzbee-io/fizzbee-mbt-examples

从玩具示例到真实应用

对于这个小示例，我们手写了形式化规范，以便能够确切地看到需求如何映射到模型。

对于更大的应用，你不一定需要从头编写规范。编码智能体可以帮助将需求翻译成 FizzBee，并随着需求演变而精化模型。FizzBee 为 Claude Code、Cursor 和 Gemini CLI 等 AI 编码助手提供了技能，因此智能体可以理解 FizzBee 语言、运行模型检查器、调试规范并编写基于模型的测试。

对于新应用，另一个选择是 FizzBee.ai，它会引导你完成需求工程过程。你从一个提示开始；系统会提出有针对性的问题，生成形式化规范，并使用生成的原型帮助与利益相关者验证需求。

结语

在本文中，我们看到了看似显而易见的需求如何可能留下重要行为未被指定，以及形式化规范如何快速暴露这些缺口。

更重要的是，我们看到了使需求可执行的几个实际好处：

发现需求缺口。 将需求形式化会迫使我们把隐式行为显式化，并暴露出原始需求中未明确说明的决策。
检查一致性。 我们可以探究这些需求是否能够同时被满足，并发现那些可能只在实现阶段才会浮现的矛盾。
描述随时间变化的行为。 动态逻辑为我们提供了一种描述状态变化系统的方式，而不仅仅是值之间的静态关系。
探索预期行为。 可执行规范让利益相关者能够在系统实现之前，以交互方式探索系统可能的行为。
根据规范测试实现。 同一份规范可以作为基于模型的测试的测试预言，让我们能够将实现与需求所描述的行为进行比较。

一个 .md 文件可以描述我们希望系统做什么。可执行规范能够描述它、检查它，并让我们探索它。

这就是为什么可执行形式化规范对规范驱动开发特别有吸引力。目标不是用一堆形式化符号取代需求文档。目标是把需求转化为一种人类和机器都能推理的产物。

无论需求是用 EARS 还是普通英语编写的，形式化规范都不会取代它们；它是在检查它们。最终需求和检查它们的规范都在本文末尾，并带有标记，使每条需求都映射到强制执行它的代码。

在接下来的文章中，我们将研究更复杂的示例、指定 UX 属性的方法、更详细的基于模型的测试，以及从规范生成 UX 原型。

最终规范

EARS 格式：

R1:  THE SYSTEM SHALL allow the stylist to set their work schedule.

R1b: WHEN the stylist changes their work schedule,
     THE SYSTEM SHALL cancel any appointments outside the new schedule.

R2:  WHILE the slot is not booked, 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.

R2c: IF a customer requests a slot that is already booked,
     THEN THE SYSTEM SHALL reject the request.

R3:  THE SYSTEM SHALL ensure that all appointments are within the stylist's schedule.

R4:  WHEN a customer requests to cancel their own appointment,
     THE SYSTEM SHALL cancel it.

R4b: IF a customer requests to cancel an appointment that is not theirs,
     THEN THE SYSTEM SHALL reject the cancellation request.

FizzBee：

在 FizzBee Playground 中打开

role Stylist:
    atomic action SetSchedule:                    # R1: always enabled
        working = oneof [False, True]
        system.set_schedule(working)

role Customer:
    atomic action BookAppointment:
        system.book(self.__id__)

    atomic action CancelAppointment:
        system.cancel(self.__id__)

role System:
    action Init:
        self.scheduled_to_work = False
        self.appointment_booked = None            # customer ID when booked

    atomic func set_schedule(working):
        self.scheduled_to_work = working
        if self.appointment_booked and not self.scheduled_to_work:
            self.appointment_booked = None        # R1b: cascade cancel

    atomic func book(customer_id):                # R2
        require self.scheduled_to_work            # R2b
        require not self.appointment_booked       # R2c
        self.appointment_booked = customer_id

    atomic func cancel(customer_id):              # R4
        require self.appointment_booked == customer_id   # R4b
        self.appointment_booked = None

action Init:
    system = System()
    stylist = Stylist()
    customers = []
    for _ in range(2):
        customers.append(Customer())

always assertion BookingsInSchedule:              # R3
    return not system.appointment_booked or system.scheduled_to_work

transition assertion NoOverwritingAppointment(before, after):   # R2c
    return ((not before.system.appointment_booked)
            or (not after.system.appointment_booked)
            or (before.system.appointment_booked == after.system.appointment_booked))