# 爱国者宰赫兰：忠实执行了不再成立的假设

向软件使命时代进军 · 方法经 案-04 / 13

本文独立成篇。作者 陈鹏 · 二〇二六年十月

![封面](https://kos-tl.github.io/cases/cover-c04.png)

> 关节：软件可以忠实执行设计时的假设，却把人留在已经过期的正确性里。不能误读成 Patriot 系统「算错了」。它按当时的时钟模型算对了。世界已经不在那个模型里。

## 经过

1991 年 2 月 25 日，海湾战争期间，一枚伊拉克「飞毛腿」导弹击中沙特阿拉伯宰赫兰的美军兵营。爱国者导弹拦截系统本应拦截这枚来袭导弹，却因软件时钟累积误差导致目标跟踪失败。二十八名美军士兵死亡。这不是一次「没写对」的事故。代码忠实执行了设计时的假设。假设已经不再成立。

相邻概念必须被拆开。第一章用 Therac-25 说明信任从硬件转到软件。那是一次托付转移：物理互锁被撤掉，剂量交给程序。爱国者导弹拦截系统在宰赫兰错过拦截，不是同一类失败。时钟累积误差让目标跟踪偏离。代码没有背叛设计。它按当时的假设执行了。世界已经不在那个假设里。正确性是有有效期的。

形式化方法可以证明一段程序符合给定规范，这是正确性。它不自动等于这段程序仍在执行托付。规范可以写错，规范可以过期。正确性是必要条件，不是使命。把正确性当使命，是把绳子交给一份已经过期的说明书。


![忠实执行了不再成立的假设](https://kos-tl.github.io/cases/fig-c04-pass.png)

## 剖析

定义这一步在设计时是清楚的：拦截来袭的飞毛腿，保护兵营。禁区是不得把跟踪窗口对准一个已经漂移的位置。禁区写在设计假设里——时钟精度足以支撑连续运行若干小时。持续开机的时间越过那一截，假设就不再是假设，是一份过期的许可证。使命绑定要求验证覆盖运行中的这一次，而不是覆盖出厂那一次。

对齐失败发生在时间轴上，而不是发生在模块之间。写下的规范、编出的代码、跑着的跟踪循环，彼此对齐。它们与世界上那枚飞毛腿的真实位置不对齐。接口契约可以全部满足。时间把契约的前提抽走了。这比「两边各写各的单位」更难看见：表面上没有任何接口破裂。破裂的是「系统被允许连续运行多久」这一条从未被当作运行时的检查。

达成若等于雷达还在转、拦截程序还在循环，那天系统达成了。它达成的是一份过期的正确性。托付者是兵营里的士兵。软件执行托付。当假设过期，执行越忠实，后果越确定。

人的三个位置在战时被压缩。立法把拦截写成任务。划界本应规定：开机超过某一时长必须重新校准、必须切换、必须停机人工确认。审判本应能在累积误差越过阈值时拒绝继续自动拦截。把士兵留在已经过期的自动循环里，不是让机器承担使命，是让人在最没有干预余地的位置上承担后果。

分级上，这是关键执行级。自主执行不可逆、高影响的拦截决策，要求运行中确认，而不是出厂证明。出厂证明回答「按这份规范，它当时是对的」。运行中确认回答「这一秒，规范的前提还在不在」。少了后一句，高峰停在实验室。

它也钉住方法学的一条边界。方法论必须能失败。如果一份方法只能证明「符合规范」，不能说出「规范的哪一条前提已经过期」，它会把过期的正确性当成完成。假使命可以寄生在方法里：方法越完整，过期的假设越像一份合格证明。


![正确性有有效期，验证必须覆盖运行中的这一次](https://kos-tl.github.io/cases/fig-c04-cut.png)

## 对方法的一针

> 正确性有有效期。验证必须覆盖运行中的这一次。假设必须被写成可过期的对象：超时、越界、连续运行过长，都应变成拒绝继续自动执行的检查，而不是事后调查里才被发现的前提。士兵是托付者。软件执行托付，不签发过期的正确性。

---

知识操作系统是架构主张，不是已经交付的操作系统。使命软件工程学尚没有形成。

详细论证、数据口径与未解清单，见同题专著《向软件使命时代进军》第13稿。

在线阅读：檄文 [kos-tl.github.io](https://kos-tl.github.io/index.html?lang=zh) · 专著 [kos-tl.github.io/book](https://kos-tl.github.io/book/) · 体系图 [kos-tl.github.io/system](https://kos-tl.github.io/system/) · 典型案例 [kos-tl.github.io/cases](https://kos-tl.github.io/cases/)

上一篇：《Knight Capital：四十五分钟的假达成》　下一篇：《火星气候轨道器：各自正确，合起来是错的》

https://kos-tl.github.io/cases/patriot/