关键环境下Ada契约式设计疑问：除法函数契约与容错实现抉择

问题本质 #

你碰到的是关键安全系统里，契约式设计的“开发期校验”定位，和系统“故障绝对可控”要求的核心冲突——Ada的前置条件本来是给开发、测试阶段用的，但生产环境禁用后，一旦客户端违规传参，就会触发不可控的约束错误，这在关键环境里是绝对不能接受的。

要不要防这类人为失误？ #

必须防，而且是生产环境的强制要求：

• 关键环境（航空、医疗、核电这类）的底线是故障不能扩散，必须按预设流程处理。哪怕是客户端的低级错误（传0当除数），也不能放任程序抛出未处理的约束错误——这种错误可能直接导致系统崩溃、数据丢失，甚至引发安全事故。
• 契约的前置条件本质是开发文档+测试期校验工具，不是生产环境的防护手段。测试阶段能靠契约抓违规，但生产环境禁用契约后，没有兜底检查的话，违规传参就是定时炸弹。

要不要牺牲性能做每次检查？ #

完全不用纠结，因为：

• 性能损耗微乎其微：浮点数是否为0的检查是单指令级操作，纳秒级耗时，对绝大多数关键系统来说，这点开销完全可以忽略——相比不可控故障的代价，这点性能牺牲根本不值一提。
• 可以用编译开关做按需检查：结合Ada的条件编译，让检查只在生产环境生效，测试环境靠契约校验：

  function div (dividend, divisor : Float) return Float
  with Pre => divisor /= 0;
  
  function div (dividend, divisor : Float) return Float is
  begin
      -- 测试环境依赖契约前置条件，生产环境保留显式检查
      #if PRODUCTION then
          if divisor = 0 then
              InconsistencyManager.inconsistency ("Divisor zero in div()");
          end if;
      #end if;
      return dividend / divisor;
  end div;
  

  这样既不影响测试阶段的契约校验，又能在生产环境提供兜底防护，还能让测试环境的性能不受影响。

关于函数副作用的顾虑 #

你觉得显式检查带副作用怪异，其实可以用异常处理解耦：

• 把错误检查和故障处理分开，函数只负责抛出异常，统一在异常处理块里调用不一致管理模块：

  exception Divisor_Zero : others;
  
  function div (dividend, divisor : Float) return Float is
  begin
      if divisor = 0 then
          raise Divisor_Zero with "Invalid divisor: zero";
      end if;
      return dividend / divisor;
  exception
      when Divisor_Zero =>
          InconsistencyManager.inconsistency ("Divisor zero in div()");
          -- 这里可以选择进入安全循环，或者根据系统要求处理
          loop null; end loop;
  end div;
  

  这样函数的核心逻辑（除法）保持纯净，故障处理逻辑被隔离在异常块里，既满足了关键环境的要求，又避免了函数直接带副作用的怪异感。

最后总结 #

1. 关键环境里，哪怕是客户端的人为失误，也必须有生产环境的兜底防护——契约是开发工具，不是生产防护；
2. 性能代价可以忽略，还能通过编译开关优化；
3. 用异常处理能平衡函数纯净性和故障处理需求。

内容的提问来源于stack exchange，提问作者Albatros23