形式化设计与形式化验证

优化软件的需求本来就大量使用集合、量词、等式和不等式，因此天然适合在编码前进行形式化设计，并在编码后验证“领域规则、数学表达和程序实现”是否一致。目标不是为整个系统一次性写出机器证明，而是让每条重要规则都有明确前提、可检查语义和可追溯证据。

1. 三个需要对齐的对象

对一条业务规则，区分：

层次	记号	示例
领域命题	$p$	输入点位于分片域内时，输出等于该处的分段线性曲面值
数学规格	$p_f:X\to \mathbb{B}$	$z=f_{\mathcal{T}}(x,y)$
可执行实现	$p_e:X\to \mathbb{B}$	BivariateLinearPiecewiseFunction 的三角形选择与重心插值模型

已有领域知识和前提组成集合 $K$。新增规则首先要与它一致：

$$\mathrm{SAT}(K\cup \{p_f\})⟺\mathrm{\exists }x\in X:(\underset{q\in K}{\bigwedge }q(x))\wedge p_f(x).$$

实现正确性要求：

$$K\models (p_f\iff p_e),$$

也就是：

$$\mathrm{\forall }x\in X:(\underset{q\in K}{\bigwedge }q(x))\Rightarrow (p_f(x)\iff p_e(x)).$$

没有写入 $K$ 的单位、边界、离散性或数据假设，不能在证明和测试中被偷偷使用。

2. 形式化设计流程

2.1 建立规则身份

为规则指定稳定 ID、领域名称、所有者 Context、来源和版本。规则名称应表达业务含义，例如 bandwidth.no_outflow_without_service，而不是实现序号。

2.2 声明候选宇宙与前提

明确：

• 集合、索引及空集合行为；
• 决策变量的定义域；
• 参数单位、范围和空值策略；
• 有限上下界及其推导来源；
• 严格不等式如何转换；
• 求解容差与业务容差。

2.3 写领域谓词

先写不依赖 Big-M、辅助变量或某个求解器的命题。若一条自然语言包含多个“并且”“除非”或例外，应拆成可独立命名的谓词。

2.4 推导数学实现

可以采用两条路线：

1. 从 $K$ 和 $p_f$ 演绎出可执行的 $p_e$；
2. 先提出候选 $p_e$，再证明 $K\models (p_f\iff p_e)$。

第二条路线不能停在“常见写法”或“样例能跑”；必须补齐等价条件，尤其是有限上下界和变量定义域。

2.5 映射到 OSPF 构件

• 变量由 Aggregation 或领域 Model 拥有；
• 可复用定义成为具名中间值；
• 约束由具名 Pipeline 注册；
• Context 决定在不同业务模式或求解路径中的注册组合；
• Application 只编排，不重新定义公式。

2.6 建立追溯

把命题 ID、公式、Pipeline、测试、基准数据和变更记录关联起来。任一公式变更都应能找到受影响测试和消费者上下文。

3. 等价性的验证义务

逻辑等价可以拆成两个方向：

$$\underset{\text{可靠性：实现不接受领域无效解}}{\underbrace{p_e(x)\Rightarrow p_f(x)}},\underset{\text{完备性：实现不拒绝领域有效解}}{\underbrace{p_f(x)\Rightarrow p_e(x)}}.$$

也可按规格真值拆成正、负分支：

规格 $p_f$	实现 $p_e$	结论
true	true	正分支通过
true	false	假阴性，违反完备性
false	false	负分支通过
false	true	假阳性，违反可靠性

测试不能只覆盖“应当可行”的正例。每条约束至少需要一个违反该规则且尽量满足其他前提的负例。

4. 经典推导一：二元线性分段函数

本节以 ospf-kotlin 当前的“三角剖分 + 重心插值”实现为准。它要证明的不是“若干测试点算得差不多”，而是从业务语义开始，经逻辑析取推导出线性约束，并证明符号模型的全部可行解恰好描述给定三角剖分上的分段线性曲面。

4.1 自然语言规则与前提

令 $\mathcal{T}$ 为非空三角形集合。三角形 $t\in \mathcal{T}$ 的三个三维顶点为：

$$P_{tj}=(x_{tj},y_{tj},z_{tj}),j\in \{1,2,3\}.$$

对输入 $(x,y)$ 和输出 $z$，规则是：

• $(x,y)$ 必须落在至少一个三角形的二维投影内；
• 选定一个包含 $(x,y)$ 的三角形后，$z$ 必须等于该三角形三个顶点高度的重心插值；
• 若 $(x,y)$ 不属于任何三角形，函数在该点无定义，符号模型必须不可行。

每个二维投影必须非退化：

$$D_t=(x_{t2}-x_{t1})(y_{t3}-y_{t1})-(x_{t3}-x_{t1})(y_{t2}-y_{t1})\ne 0.$$

相邻三角形若共享边或顶点，必须在共享位置上给出相同的 $z$；三角形内部不应重叠，除非重叠部分上的两个仿射平面完全一致。否则，同一个 $(x,y)$ 可能对应多个 $z$，得到的是多值关系而不是函数。

4.2 逻辑语言

先不引入选择变量。对每个三角形 $t$，定义“输入输出位于该分片上”的谓词：

$$\begin{array}{rl}{R}_t(x,y,z)\equiv & \mathrm{\exists }{\lambda }_{t1},{\lambda }_{t2},{\lambda }_{t3}\in {\mathbb{R}}_{\ge 0}:\\ & \sum _{j=1}^3{\lambda }_{tj}=1\\ & \wedge x=\sum _{j=1}^3{\lambda }_{tj}{x}_{tj}\\ & \wedge y=\sum _{j=1}^3{\lambda }_{tj}{y}_{tj}\\ & \wedge z=\sum _{j=1}^3{\lambda }_{tj}{z}_{tj}.\end{array}$$

前三个条件说明 $(x,y)$ 是投影三角形中一点，最后一个条件要求使用同一组重心权重插值高度。整个二元线性分段函数是所有三角形分支的逻辑析取：

$$p_f(x,y,z)\equiv \underset{t\in \mathcal{T}}{\bigvee }{R}_t(x,y,z).$$

这一定义同时表达了定义域：若没有任何 $R_t$ 成立，则不存在合法输出 $z$。若多个 $R_t$ 在共享边界上成立，前提中的曲面一致性保证它们给出同一个 $z$。

4.3 推导线性不等式

逻辑表达中的“至少一个分支成立”需要转换为混合整数线性模型。为每个三角形引入选择变量：

$${\delta }_t\in \{0,1\}.$$

第一步：只激活一个分片。

$$\sum _{t\in \mathcal{T}}{\delta }_t=1.$$

若求解器的标准形式只保留不等式，该等式等价于：

$$\sum _t{\delta }_t\le 1,-\sum _t{\delta }_t\le -1.$$

第二步：激活对应的重心权重。 为每个顶点引入 ${\lambda }_{tj}\ge 0$，并令：

$$\sum _{j=1}^3{\lambda }_{tj}={\delta }_t,\mathrm{\forall }t\in \mathcal{T}.$$

当 ${\delta }_t=0$ 时，非负性与权重和共同推出该分片全部权重为 0；当 ${\delta }_t=1$ 时，权重非负且和为 1。其纯不等式形式为：

$$\sum _j{\lambda }_{tj}-{\delta }_t\le 0,{\delta }_t-\sum _j{\lambda }_{tj}\le 0.$$

第三步：合并各分支的坐标与高度。

定义：

$$A_x(\lambda )=\sum _{t\in \mathcal{T}}\sum _{j=1}^3{\lambda }_{tj}{x}_{tj},$$$$A_y(\lambda )=\sum _{t\in \mathcal{T}}\sum _{j=1}^3{\lambda }_{tj}{y}_{tj},A_z(\lambda )=\sum _{t\in \mathcal{T}}\sum _{j=1}^3{\lambda }_{tj}{z}_{tj}.$$

关联输入输出：

$$x=A_x(\lambda ),y=A_y(\lambda ),\hat{z}=A_z(\lambda ).$$

每个等式 $v=A_v(\lambda )$ 都可以展开为一对线性不等式：

$$v-A_v(\lambda )\le 0,A_v(\lambda )-v\le 0,v\in \{x,y,\hat{z}\}.$$

至此，逻辑析取已经被完整转换为二值变量、非负变量以及线性不等式。该推导不需要任意取大的 Big-M。ospf-kotlin 中，zVars 承担 ${\delta }_t$ 的角色，lambdaVars 承担 ${\lambda }_{tj}$ 的角色。

4.4 等价性证明

可靠性 $p_e\Rightarrow p_f$： 由 $\sum _t{\delta }_t=1$ 且 ${\delta }_t$ 为二值变量，恰有一个三角形 $t^{\star }$ 被选中。对所有 $t\ne t^{\star }$：

$$\sum _j{\lambda }_{tj}={\delta }_t=0.$$

结合 ${\lambda }_{tj}\ge 0$，这些三角形的所有权重均为 0。对 $t^{\star }$，权重非负且和为 1；输入和输出关联式随即满足 $R_{t^{\star }}(x,y,\hat{z})$，因此 $p_f(x,y,\hat{z})$ 成立。

完备性 $p_f\Rightarrow p_e$： 若 $p_f(x,y,z)$ 成立，则至少存在一个三角形 $t^{\star }$ 及一组使 $R_{t^{\star }}(x,y,z)$ 成立的重心权重。令 ${\delta }_{t^{\star }}=1$、其余选择变量为 0；保留该分片的权重并把其余权重设为 0，即可满足全部线性约束。

因此在非退化与重叠一致性前提 $K_{\mathcal{T}}$ 下：

$$K_{\mathcal{T}}\models (p_f(x,y,z)\iff p_e(x,y,z)).$$

可靠性保证模型不接受定义域外或插值错误的点；完备性保证逻辑规格允许的每个曲面点都能由线性模型表示。

4.5 从证明得到的测试

使用三角形：

$$P_1=(0,0,0),P_2=(1,0,1),P_3=(0,1,1).$$

该分片上的曲面为 $z=x+y$。因此 $(x,y)=(0.25,0.25)$ 的正确结果是：

$$z=0.5.$$

验证至少覆盖：

类别	输入	应验证
三个顶点	$P_1,P_2,P_3$	权重 one-hot，结果等于顶点高度
内部点	$(0.25,0.25)$	三个权重非负且和为 1，$z=0.5$
共享边	一个权重为 0	相邻分片给出相同 $z$，顺序不影响结果
域外点	不属于任何三角形	直接求值返回空，符号模型不可行
退化三角形	$D_t=0$ 或接近 0	构造/求值按契约拒绝，不参与证明
重叠分片	同一 $(x,y)$ 属于多个内部	要么拒绝，要么证明重叠处高度一致
双路径一致性	同一输入	evaluate 结果与 solver 固定输入后的 $\hat{z}$ 一致

更多 API 与边界见二元线性分段函数。

5. 经典推导二：建议载重量

这个例子关注一条业务规则如何逐层收敛为可执行约束，而不讨论代码复用或中间值的实现方式。

5.1 自然语言规则

对每个装载位置 $p$：

• 若该位置未被选为建议装载位置，则其建议载重量必须为 0；
• 若该位置被选中，则其建议载重量必须处于允许区间 $[{\underset{―}{W}}_p,{\bar{W}}_p]$；
• 允许区间必须使用统一的重量单位，并满足 $0<{\underset{―}{W}}_p\le {\bar{W}}_p$。

自然语言中的“若……则……”和“处于区间”必须先转换为逻辑命题，不能直接跳到 Big-M 约束。

5.2 逻辑语言

定义：

$$u_p\in \{0,1\}$$

表示位置 $p$ 是否被选中，$w_p\in {\mathbb{R}}_{\ge 0}$ 表示其建议载重量。自然语言规则对应的领域谓词为：

$$p_f(u_p,w_p)\equiv (u_p=0\wedge w_p=0)\vee (u_p=1\wedge {\underset{―}{W}}_p\le w_p\le {\bar{W}}_p).$$

也可以写成两条蕴含：

$$u_p=0\Rightarrow w_p=0,$$$$u_p=1\Rightarrow {\underset{―}{W}}_p\le w_p\le {\bar{W}}_p.$$

因为 $u_p$ 是二值变量，两种状态互斥且完备。正下界 ${\underset{―}{W}}_p>0$ 还保证 $w_p>0$ 当且仅当 $u_p=1$；若业务允许“选中但建议重量为 0”，应把下界改为 0，并删除这一双向解释。

5.3 推导线性不等式

先处理上界。两种逻辑状态所要求的上界分别为：

$$u_p=0:w_p\le 0,$$$$u_p=1:w_p\le {\bar{W}}_p.$$

由于 $u_p\in \{0,1\}$，它们可以合并为：

$$w_p\le {\bar{W}}_p{u}_p.$$

再处理下界。两种状态所要求的下界分别为：

$$u_p=0:w_p\ge 0,$$$$u_p=1:w_p\ge {\underset{―}{W}}_p.$$

它们可以合并为：

$$w_p\ge {\underset{―}{W}}_p{u}_p.$$

因此最终的线性实现为：

$$p_e(u_p,w_p)\equiv {\underset{―}{W}}_p{u}_p\le w_p\le {\bar{W}}_p{u}_p.$$

这里的 ${\bar{W}}_p$ 不是任意取大的 Big-M，而是位置 $p$ 的有效业务上界；${\underset{―}{W}}_p$ 同样是规格的一部分。

5.4 等价性证明

可靠性 $p_e\Rightarrow p_f$：

• 若 $u_p=0$，线性约束化为 $0\le w_p\le 0$，所以 $w_p=0$；
• 若 $u_p=1$，线性约束化为 ${\underset{―}{W}}_p\le w_p\le {\bar{W}}_p$。

两个二值分支都满足领域谓词，因此线性实现不会接受违反规则的解。

完备性 $p_f\Rightarrow p_e$：

• 若领域状态为 $u_p=0\wedge w_p=0$，代入后得到 $0\le 0\le 0$；
• 若领域状态为 $u_p=1\wedge {\underset{―}{W}}_p\le w_p\le {\bar{W}}_p$，代入后恰好得到原区间。

因此在前提

$$u_p\in \{0,1\},0<{\underset{―}{W}}_p\le {\bar{W}}_p$$

下，有：

$$K_{\mathrm{weight}}\models (p_f(u_p,w_p)\iff p_e(u_p,w_p)).$$

5.5 从证明得到的测试

设 ${\underset{―}{W}}_p=100\mathrm{kg}$、${\bar{W}}_p=500\mathrm{kg}$，至少覆盖：

$u_p$	$w_p$	期望	验证分支
0	$0$	可行	未选中的正例
0	$\delta$	不可行	未选中的负例
1	$100$	可行	闭区间下边界
1	$300$	可行	区间内部
1	$500$	可行	闭区间上边界
1	$100-\delta$	不可行	下界外侧
1	$500+\delta$	不可行	上界外侧

$\delta$ 必须大于求解器的可行性容差。还应验证：

• $u_p$ 被错误放宽为连续变量时，等价性测试能够失败；
• 下界、上界或重量值单位不一致时，在进入模型前被拒绝或换算；
• ${\underset{―}{W}}_p>{\bar{W}}_p$ 的数据在初始化阶段被拒绝；
• 多个位置组成的小规模实例中，逐点比较 $p_f$ 与 $p_e$ 的真假值；
• 固定 $u_p,w_p$ 后，Kotlin 与 Rust 的 solver 测试得到相同可行性结论。

6. 五层验证

层次	验证对象	推荐证据
1. 领域谓词	自然语言与形式化规格一致	领域评审、真值表、反例
2. 数学推导	$K\models (p_f\iff p_e)$	代数证明、SMT/穷举、小规模反证模型
3. 符号构造	OSPF 表达式等于数学实现	系数、常数项、上下界和约束方向快照
4. 求解器契约	编译后的模型实现符号语义	微型可行/不可行模型、多后端测试
5. 应用行为	上下文组合和解分析正确	基准实例、回归集、领域不变量

层次 3 通过，不代表层次 2 正确；求解器得出预期目标，也不能代替负分支验证。

7. 一致性、冗余与冲突

向模型增加 $p$ 前，分别检查：

一致性

$$\mathrm{SAT}(K\cup \{p\}).$$

若不可满足，应给出不可满足核心或最小冲突规则集，并用领域名称报告。

冗余

$$K\models p.$$

冗余约束不改变可行域。它可能为了强化 LP、提高可读性或诊断而保留，但应记录目的，避免误认为它增加了业务规则。

冲突

$$K\models \mathrm{\neg }p.$$

这说明新增规则否定了所有既有可行情况。若这是业务变更，应同步更新被替代的规则和基准，而不是简单叠加。

8. 数值语义

形式化规格使用精确关系，浮点求解器使用容差。验证报告必须同时给出：

• 规格关系，例如 $g(x)\le b$；
• 求解器容差 ${\epsilon }_s$；
• 测试判定容差 ${\epsilon }_t$；
• 业务容差 ${\epsilon }_b$；
• 变量缩放和单位。

不要使用正好落在容差灰区内的数值作为唯一负例。测试等式时，应分别覆盖 $b-\delta$、$b$、$b+\delta$，并说明哪些值属于业务有效、数学有效和求解器可接受。

9. 分解算法中的验证

列生成

需要证明 Pricing 的领域可行列与 Master 接受的列定义一致，并验证：

$${\overline{c}}_p=c_p-\sum _i{\pi }_i{a}_{ip}$$

在两侧使用同一成本、系数和对偶符号约定。小实例上应与完整列枚举比较。

Benders

需要证明选择性注册与完整模型等价、固定变量映射保持语义，以及每条切割对所有原问题可行解都有效。可行性切割必须排除当前不可行主解；最优性切割必须在生成点提供正确的追索下界。

10. 变更控制

规则变更时按以下顺序处理：

1. 更新领域命题、前提和版本；
2. 重新检查一致性、冗余和受影响推论；
3. 更新数学推导及中间值接口；
4. 修改 Pipeline 或函数符号实现；
5. 从新的证明分支更新测试；
6. 运行上下文、完整模型、分解模型和后端回归；
7. 在发布说明中记录可行域或目标语义是否变化。

如果只优化实现而不改变 $p_e$ 的真值集合，属于保持语义的重构；如果真值集合变化，就必须按领域规则变更处理。

11. 完成标准

一条规则只有同时满足以下条件才算完成：

• 有稳定 ID、所有者和业务描述；
• 前提、单位、定义域与容差完整；
• 数学规格和可执行表达均已记录；
• 等价性的两个方向有证明或足够的可检查证据；
• 正、负、边界和异常输入测试齐全；
• 能从文档追溯到中间值、Pipeline、测试和基准；
• 在实际使用的求解器后端上通过契约测试。

12. 相关内容

• 数学模型的演绎逻辑表达
• DDD 基础架构
• DDD 与列生成
• DDD 与 Benders 分解