BDD语义化升级：Gherkin到形式化规格的自动转换
TL;DR
003e 本文核心观点：
- Gherkin的局限 — 自然语言描述的验收标准存在歧义，无法自动验证
- 形式化规格 — 用数学精确描述行为，实现真正的可执行规格
- AI桥梁 — LLM可以将自然语言Gherkin自动转换为形式化表达
- 闭环验证 — 规格生成代码，代码反验证规格，形成自洽系统
📋 本文结构
- Gherkin的天花板 — 为什么自然语言不够
- 形式化规格入门 — 用数学描述行为
- AI自动转换 — Gherkin → 形式化规格 → 代码
- 闭环验证系统 — 规格与代码的双向约束
- 工具链实践 — 可落地的工程方案
- 结论 — 行为驱动的新纪元
Gherkin的天花板
💡 Key Insight
003e Gherkin让非技术人员能读验收标准，但”能读”不等于”能精确执行”。自然语言的模糊性是系统Bug的重要来源。
经典Gherkin示例
Feature: 订单折扣计算
Scenario: VIP客户享受折扣
Given 一个VIP客户
When 他下单购买$100的商品
Then 他应该支付$90
看起来清晰，但魔鬼在细节：
| 模糊点 | 可能解释A | 可能解释B | 可能解释C |
|---|---|---|---|
| “VIP客户” | 积分≥1000 | 购买过3次以上 | 订阅了会员服务 |
| “$100的商品” | 原价$100 | 折扣前$100 | 一件商品$100 |
| “支付$90” | 最终金额$90 | 折扣$10 | 还需加税 |
| “VIP” | 终身VIP | 当月VIP | 特定等级VIP |
这些歧义在实际开发中需要反复确认，每次确认都是时间和认知成本。
为什么模糊性是问题
产品经理写的Gherkin
↓
开发者理解A版本
↓
测试人员理解B版本
↓
验收时发现不一致
↓
开会澄清（30分钟）
↓
修改实现（2小时）
↓
重新测试（1小时）
每次模糊点平均消耗3-4小时。
形式化规格入门
💡 Key Insight
003e 形式化规格不是给机器看的，而是给所有人一个无可争议的事实来源。数学是唯一的通用语言。
什么是形式化规格
用数学符号精确描述系统行为，消除所有自然语言歧义。
非形式化：
"订单金额大于$50免运费"
半形式化（结构化）：
condition: order.total_amount > 50
action: shipping_fee = 0
完全形式化（数学表达式）：
∀ order ∈ Orders:
order.total_amount > 50 → order.shipping_fee = 0
常用形式化方法
| 方法 | 适用场景 | 示例 |
|---|---|---|
| 谓词逻辑 | 状态约束 | ∀x (P(x) → Q(x)) |
| 时序逻辑 | 事件顺序 | ◇(A ∧ ○B) 最终A且接下来B |
| 状态机 | 状态转换 | State × Event → State |
| 代数规格 | 数据结构 | push(pop(stack)) = stack |
| 合约式 | 前置/后置条件 | requires: x > 0; ensures: result > 0 |
TLA+示例：简单规格
(* 订单状态机规格 *)
MODULE Order
EXTENDS Integers, Sequences, FiniteSets
CONSTANTS Items, Customers
VARIABLES orders, orderCounter
(* 类型不变式 *)
TypeInvariant ==
orders ⊆ [id: Nat,
customer: Customers,
items: SUBSET Items,
status: {"created", "paid", "shipped", "delivered", "cancelled"}]
(* 初始状态 *)
Init ==
orders = {}
orderCounter = 0
(* 创建订单 *)
CreateOrder(c, i) ==
orderCounter' = orderCounter + 1
orders' = orders ∪ {[id ↦ orderCounter',
customer ↦ c,
items ↦ i,
status ↦ "created"]}
(* 支付订单 *)
PayOrder(o) ==
o ∈ orders
o.status = "created"
orders' = (orders \\ {o}) ∪
{[id ↦ o.id,
customer ↦ o.customer,
items ↦ o.items,
status ↦ "paid"]}
UNCHANGED orderCounter
(* 状态转换 *)
Next ==
∃ c ∈ Customers, i ∈ SUBSET Items: CreateOrder(c, i)
∨ ∃ o ∈ orders: PayOrder(o)
(* 系统规格 *)
Spec == Init ∧ □[Next]_⟨orders, orderCounter⟩
这个规格可以被TLC模型检查器验证，确保没有死锁、状态不一致等问题。
AI自动转换
💡 Key Insight
003e LLM的强项是理解自然语言，形式化方法的强项是精确表达。两者结合：LLM将Gherkin翻译为形式化规格，再翻译为可执行代码。
转换Pipeline
┌─────────────────────────────────────────┐
│ 输入: Gherkin自然语言描述 │
│ │
│ Given 一个VIP客户 │
│ When 他下单购买$100的商品 │
│ Then 他应该支付$90 │
└─────────────────────────────────────────┘
↓
┌─────────────────────────────────────────┐
│ 步骤1: 歧义识别与澄清 │
│ │
│ AI检测: "VIP客户"定义不明确 │
│ 询问: VIP的判断标准是什么？ │
│ 回答: 积分≥1000 │
└─────────────────────────────────────────┘
↓
┌─────────────────────────────────────────┐
│ 步骤2: 转换为结构化规格 │
│ │
│ preconditions: │
│ - customer.points >= 1000 │
│ - order.original_amount == 100 │
│ - discount_rate = 0.1 │
│ postconditions: │
│ - order.final_amount == 90 │
└─────────────────────────────────────────┘
↓
┌─────────────────────────────────────────┐
│ 步骤3: 生成形式化表达式 │
│ │
│ ∀ c ∈ Customer, o ∈ Order: │
│ c.points ≥ 1000 ∧ o.amount = 100 │
│ → o.final = 90 │
└─────────────────────────────────────────┘
↓
┌─────────────────────────────────────────┐
│ 步骤4: 生成可执行代码+测试 │
│ │
│ def calculate_total(customer, order): │
│ if customer.points >= 1000: │
│ return order.amount * 0.9 │
│ return order.amount │
└─────────────────────────────────────────┘
实战：转换示例
输入Gherkin：
Scenario: 并发订单不超卖
Given 商品A库存为10
When 100个用户同时下单购买商品A
Then 最多只有10个订单能成功
And 所有成功的订单加起来不能超过10件
AI转换过程：
步骤1: 识别关键概念
- 库存: inventory[product_id] = quantity
- 订单: order[order_id] = {product, quantity, status}
- 并发: 多个操作同时发生
步骤2: 识别约束条件
- 全局不变式: Σ successful_orders.quantity ≤ inventory
- 原子性: 库存检查与扣减必须一起完成
步骤3: 形式化规格(TLA+)
```tla
(* 库存不变式 *)
InventoryInvariant ==
∀ p ∈ Products:
LET sold = Sum({o.quantity : o ∈ orders ∧ o.product = p ∧ o.status = "success"})
IN sold ≤ inventory[p]
(* 并发操作的原子性 *)
PlaceOrder(c, p, q) ==
LET available = inventory[p] - Sum({o.quantity : o ∈ orders ∧ o.product = p ∧ o.status = "success"})
IN IF available >= q
THEN orders' = orders ∪ {[customer ↦ c, product ↦ p, quantity ↦ q, status ↦ "success"]}
ELSE orders' = orders ∪ {[customer ↦ c, product ↦ p, quantity ↦ q, status ↦ "failed"]}
步骤4: 生成实现代码
@transaction.atomic
def place_order(customer_id, product_id, quantity):
# SELECT FOR UPDATE 保证原子性
product = Product.objects.select_for_update().get(id=product_id)
sold = Order.objects.filter(
product=product,
status='success'
).aggregate(Sum('quantity'))['quantity__sum'] or 0
available = product.inventory - sold
if available >= quantity:
order = Order.objects.create(
customer_id=customer_id,
product=product,
quantity=quantity,
status='success'
)
return order
else:
Order.objects.create(
customer_id=customer_id,
product=product,
quantity=quantity,
status='failed'
)
raise InsufficientInventory()
步骤5: 生成验证测试
def test_concurrent_orders_no_oversell():
# 设置库存
product = Product.objects.create(inventory=10)
# 并发执行100个订单请求
with ThreadPoolExecutor(max_workers=100) as executor:
futures = [
executor.submit(place_order, i, product.id, 1)
for i in range(100)
]
results = [f.result() for f in futures]
# 验证
successful = [r for r in results if r.status == 'success']
total_sold = sum(o.quantity for o in successful)
assert len(successful) <= 10
assert total_sold <= 10
---
## 闭环验证系统
> 💡 **Key Insight**
>
003e 规格与代码应该是双向约束的：规格生成代码，代码反验证规格。任何不一致都说明理解偏差。
### 双向验证模型
自然语言需求
↓
┌─────────────────────┐
│ AI转换引擎 │
│ (Gherkin → 形式化) │
└─────────────────────┘
↓
形式化规格
↙ ↘
↓ ↓ 代码生成器 模型检查器
↓ ↓ 可执行代码 性质验证报告
↓ ↓
┌─────────────────────┐
│ 运行时监控 │
│ (检测规格违反) │
└─────────────────────┘
↓
偏差报告 → 反馈给规格 ```
运行时验证
# 规格作为装饰器
@invariant("balance >= 0")
@requires("amount > 0")
@ensures("balance == old(balance) - amount")
def withdraw(account, amount):
account.balance -= amount
return account.balance
# 运行时自动检查
class Account:
def __init__(self):
self.balance = 100
@precondition(lambda self, amount: amount > 0)
@postcondition(lambda result, self, amount: self.balance >= 0)
def withdraw(self, amount):
if amount > self.balance:
raise InsufficientFunds()
self.balance -= amount
return self.balance
工具链实践
💡 Key Insight
003e 形式化方法不是银弹，但结合AI后，它可以成为日常工程工具。关键是选择合适的工具级别。
工具选择矩阵
| 复杂度 | 工具 | 学习成本 | 适用场景 |
|---|---|---|---|
| 低 | Dafny/Contracts | 1周 | 单个函数验证 |
| 中 | Alloy | 2-4周 | 数据结构/状态机 |
| 高 | TLA+ | 1-3月 | 分布式系统 |
| 超高 | Coq/Isabelle | 数月 | 安全关键系统 |
AI增强BDD工具链
┌─────────────────────────────────────────┐
│ Feature文件 (Gherkin) │
│ 自然语言描述业务场景 │
└─────────────────────────────────────────┘
↓
┌─────────────────────────────────────────┐
│ SpecAI (LLM转换层) │
│ - 歧义检测 │
│ - 结构化转换 │
│ - 形式化生成 │
└─────────────────────────────────────────┘
↓
┌─────────┴─────────┐
↓ ↓
┌─────────────────┐ ┌─────────────────┐
│ 形式化规格 │ │ 可执行测试 │
│ - TLA+/Alloy │ │ - 单元测试 │
│ - 模型检查 │ │ - 集成测试 │
└─────────────────┘ └─────────────────┘
↓ ↓
┌─────────────────┐ ┌─────────────────┐
│ 性质验证报告 │ │ 测试报告 │
│ - 死锁检测 │ │ - 覆盖率 │
│ - 不变式检查 │ │ - 边界条件 │
└─────────────────┘ └─────────────────┘
渐进式采用策略
阶段1：增强Gherkin（1-2周）
- 使用结构化Given-When-Then
- 添加显式约束注释
- AI辅助歧义检测
阶段2：轻量形式化（1-2月）
- 关键业务流程使用合约式编程
- 生成运行时断言
- 边界条件自动枚举
阶段3：模型检查（3-6月）
- 核心状态机使用TLA+
- 并发场景模型验证
- 规格-代码一致性检查
结论
🎯 Takeaway
| 传统BDD | AI增强BDD |
|---|---|
| Gherkin是终点 | Gherkin是起点 |
| 自然语言描述 | 自然语言 → 形式化规格 → 代码 |
| 人工验证 | 自动模型检查+运行时验证 |
| 测试与规格分离 | 规格即测试，测试即规格 |
| 歧义靠沟通解决 | 歧义靠形式化消除 |
BDD的初衷是让业务、开发、测试三方对齐。形式化规格让这种对齐可验证、可自动化。
AI不是取代BDD，而是让BDD从”行为驱动开发”进化为”行为驱动工程“——从想法到可验证的实现，端到端自动化。
“规格越精确，实现越自由。形式化不是束缚，而是给创造力明确的边界。”
📚 延伸阅读
经典案例
- AWS使用TLA+验证S3和DynamoDB核心算法：形式化方法在大规模系统的实践
- Microsoft的Dafny项目：合约式编程的生产环境应用
本系列相关
- TDD的死亡与重生 (第1篇)
- SDD 2.0：用户故事的Prompt工程化 (第2篇)
- DDD meets LLM (第3篇)
学术理论
- 《Specifying Systems》(Leslie Lamport): TLA+权威教材
- 《Software Abstractions》(Daniel Jackson): Alloy方法指南
- 《The B-Method》(Abrial): 形式化方法经典
- 《Design by Contract》(Bertrand Meyer): 合约式设计奠基论文
AI-Native软件工程系列 #4 深度阅读时间：约 14 分钟
💬 评论
💡 使用 GitHub 账号登录 即可参与讨论