--- name: formal-guard description: 定义期第 4 步，形式化守护：碰到状态与操作就做偏函数定义与全化表；设计里出现较高性能要求、数据生命周期或状态机、并发与池化、跨领域边界要守的性质时，代理提出模型检查与证明的建议，人确认后数理建模、定理与证明，实施时转契约测试。四类触发之一出现，或人说「这块靠测试守不住」「证明一下」时加载。纯文档、纯界面、无状态无并发的改动不加载。 --- # 形式化守护 靠测试守不住的性质交给证明与模型检查，测试仍负责找出缺陷，两者不互相替代。每个结论带证据，证据要真的检验了它声称检验的东西。做法加载技能 `think-evidence`。形式化定义的是实现的形状，所以放在实施之前；这一步的产出就是思维模型 `think-model-first` 的模型。 本技能分两档。偏函数定义与全化表便宜，碰到状态与操作就做，不需要人确认。模型检查与证明贵，按下面四类触发，代理建议、人确认后才做。 ## 触发条件 出现下面任何一项，先判断要不要模型检查与证明，再实施： | 类别 | 典型位置 | 靠测试守不住的原因 | | --- | --- | --- | | 较高的性能要求 | 热路径、仓储的写入与查询、池 | 测试只量样本输入，上界要靠模型或论证 | | 数据生命周期、状态机、状态转移 | 会话、任务、连接、资源的生灭 | 坏顺序的组合数远超用例数 | | 并发、多线程、协程、池化 | 共享状态、取消、超时、重试 | 交错不可穷举，偶发失败复现不了 | | 跨领域协调边界上要守住的性质 | 接缝上的组合保证 | 几个局部成功不等于整体成立 | ## 谁判断 全化表不经这一关，碰到状态与操作就做，写进细化设计或开工包。模型检查与证明经这一关：代理按四类触发给出建议，填[形式化触发建议单](formal-trigger-template.md)的前半：命中哪一类、要守的性质、建议的工具与做法、预估成本、不做的后果。人确认后才投入。形式化成本不低，判错方向会浪费一程。确认不投入的，理由写进单子，性质退回只靠测试并在 spec 的「不能声称的事」里写明。 ## 怎样做 ### 偏函数定义并全化 碰到状态与操作就做这一步，不等四类触发，也不需要人确认。先把状态与操作写成偏函数并全化，再翻成领域模型与对象模型。做法加载技能 `think-model-first`。 把每个操作写成偏函数：定义域是允许的前置状态，定义域之外怎样处理（拒绝、幂等返回、显式错误），不变式排除的写不可达。全化之后每个输入都有确定的输出。状态多、表大时，先看状态里是不是缠着几条独立的轴，拆成几张小表。先拆出独立变化的轴，交叉成表逐格看。做法加载技能 `think-orthogonal`。全化表交给 `detailed-domain-design` 翻译，不照着它直接写代码。状态名与操作名取自统一语言，翻译时才对得上。 ### 数理建模与证明 让问题选工具： - 事件会不会以坏顺序发生，用模型检查器在设计的小模型上穷举，TLA+ 是默认。加载技能 `pstack:create-formal-verification-skill`，它选工具、生成项目内的验证技能，并要求先在一个故意破坏的变体上证明检查能失败。 - 代码对每个输入是否都对（内存安全、溢出、数据结构不变式），用在代码上跑的验证器；没有就用生成输入测真实代码，不用手写模型替代。 - 性质要在任何规模下成立、上界不够，才需要证明。 模型要真实于代码：模型里每个不可分步骤对应代码里一个不可分步骤，名字取自代码。模型通过的只是模型与上界，不是整个系统；说清验证了什么、在什么前提和上界下、留下了什么。 TLA+ 的结果读成状态图并讲成人能懂的路径，加载技能 `pstack:statechart`。模型报出的每条坏路径回到真实代码重放一次，重放不出来先怀疑模型。 ### 性质保持可用 数学论证、有限模型、机器证明和真实实现符合性分别记录，不混成一个「已证明」。证明工具正常退出不等于目标已证明；不自行增删公理、前提或目标。代码变化之后模型可能失真，加载技能 `pstack:maintain-formal-verification-skill`，把模型、性质同步回代码，并分清是模型漂移还是代码缺陷。 ## 证明转契约测试 实施开始时，把形式化的结论转成契约测试：每条性质一个测试，断言模型给出的结论，并写明去掉哪个检查或打乱哪个顺序它会变红。契约测试守的是「实现没有偏离模型」，模型守的是「设计没有这一类缺陷」。两层都要在。转换清单写在建议单的末尾，进 spec 的「不变式对照」。 ## 产出 - 填好并经人确认的[形式化触发建议单](formal-trigger-template.md)。 - 偏函数定义与全化表。 - 形式化交接表，给 `detailed-domain-design` 翻译用：状态变量与一起要守的不变式、每个操作的定义域、定义域外的全化规则、模型里的环境假设（时钟、外部调用、失败）。名字取自统一语言。 - 模型、定理与证明件，以及能失败的证据。 - 证明到契约测试的转换清单。 ## 下一步 进入 `detailed-domain-design`，把形式化交接表翻译成领域模型与对象模型，并留精化对照表。