# 火星气候轨道器：各自正确，合起来是错的 向软件使命时代进军 · 方法经 案-05 / 13 本文独立成篇。作者 陈鹏 · 二〇二六年十月 ![封面](https://kos-tl.github.io/cases/cover-c05.png) > 关节：两个各自正确的组件，可以组成一次错误的任务。不能误读成单位换算的笑话，也不能误读成「NASA 项目管理失败」这一句空话。接口没有被写成同一套可检查的语义。绳子断在接缝上。 ## 经过 1999 年 9 月 23 日，火星气候轨道器在发射九个月后失联，调查认定它在火星大气中烧毁。故障不是来自某个写错的算法，而来自接口契约失配。一个名为 Small Forces 的软件文件中，推力数据本应以牛·秒（N·s）表示，却以磅力·秒（lbf·s）给出。地面软件使用英制，星上软件使用公制。两边各自完成了自己的工作。因为 1 磅力约等于 4.44822 牛，导航计算把实际施加的冲量严重低估。累积偏差使进入火星大气的高度远低于预期，最终解体。成本口径必须分开写：轨道器本体约 8,700 万美元，整个任务全生命周期约 3.27 亿美元。NASA 安全通报将其定性为验证与确认的失败。 一个系统由多个组件组成。每个组件都可以有自己的规范、自己的验证、自己的「正确性」。当这些组件通过接口连接时，接口本身成为正确性传递的通道。上游提供的保证（推力值，单位为磅力·秒）与下游依赖的假设（推力值，单位为牛·秒）之间存在缺口，而这个缺口在两个独立的论证中都不可见。两边都可以「通过了测试」。合起来把轨道器送进了大气层。契约若只是文档，审查可以开完，语义仍各说各话。契约必须是可以机械检查的对象。 ![各自正确，合起来是错的](https://kos-tl.github.io/cases/fig-c05-pass.png) ## 剖析 对齐是这一案的主关节。写下的、编出的、跑着的、世界上发生的，在各自模块内部可以对齐。越过接缝，语义已经不是同一件事。地面软件交出一份它按磅力·秒算对的推力。星上软件按牛·秒接收同一组数字。导航把实际冲量低估了约 4.45 倍。局部测试全部绿灯。系统测试如果只问「数据有没有传过去」，也会绿灯。绿灯覆盖的是通道，不是语义。缺口在两边各自的论证里都看不见。 定义上，托付是把轨道器送入被设计的火星轨道。禁区是不得按错误的力执行制动。禁区写在两个团队各自的单位习惯里，没有写在那一次数据交接必经的检查上。能力很强：两边都能算出、都能传、都能执行。禁区弱于能力。 达成若等于「两个子系统都交付了」，项目达成了。轨道器失踪那天，各自的里程碑早已签字。验收即结束。合同买的是两个能用的软件包，不是一份跨组件的行为论证。可组合性被当成集成测试的副产品，而不是一条必须被证明的性质。 接口契约必须进入使命绑定。契约不是文档对齐，是同一套可被机器检查的语义：单位、量纲、坐标系、时间基准、正负号、精度与有效范围。少了这一层，形式化方法在模块内越强，接缝上的错误越像「已经证明过了」。证明过的是局部。局部正确可以成为系统错误的掩护。 人的位置被拆到两个组织。立法在任务级是清楚的。划界落在两个团队的接口文档上，文档没有牙齿。审判没有一个独立位置有权说：两边单位不一致，这次交接不得进入飞控。把审查写成会议，把契约写成附件，等于没有划界。 它也钉住方法里「对齐」不能被理解成三张检查单。填完「规范一致」「代码符合规范」「测试通过」三张表，这一案仍然会发生。三张表可以各自为真。接缝上没有第四张不可绕过的检查：这一次交接的语义是否仍是同一件事。 ![契约必须覆盖单位与语义，各自正确不是系统正确](https://kos-tl.github.io/cases/fig-c05-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/) 上一篇：《爱国者宰赫兰：忠实执行了不再成立的假设》　下一篇：《CrowdStrike：保护软件成为可信计算基》 https://kos-tl.github.io/cases/mco/