Ada/SPARK中如何标记不可达代码？附线性搜索示例

针对你的线性搜索函数，由于前置条件已经保证数组中必然存在待查找元素，循环后的返回语句确实属于不可达代码。以下是Ada/SPARK中标记这类代码并支持编译器优化的推荐方式：

1. 使用pragma Unreachable;（推荐） #

Ada 2012及以上版本引入了pragma Unreachable;，它的作用是明确告知编译器：当前代码路径永远不会被执行。编译器会据此优化掉这段代码，同时也能提升代码可读性——读者一眼就能明白此处逻辑上不可达。

修改后的代码如下：

function Linear_Search (A : Elem_Array; E : Elem) return Index is
begin
   for i in A'Range loop
      pragma Loop_Invariant (for some J in i .. A'Last => A (J) = E);
      if A (i) = E then
         return i;
      end if;
   end loop;
   pragma Unreachable; -- 前置条件保证循环内必然找到元素，此处不可达
end Linear_Search;

关键说明： #

• 编译器层面：GNAT等主流Ada编译器会识别这个pragma，直接移除不可达代码，不会生成对应的机器指令。
• SPARK验证层面：由于你的代码已经有Pre => Contains(A, E)的前置条件，加上循环不变式for some J in i .. A'Last => A(J) = E，SPARK验证器可以证明循环必然会在某个迭代中找到元素并返回，因此会认可pragma Unreachable;的正确性，不会抛出验证错误。

2. 结合断言（备选） #

如果需要同时添加错误提示（比如调试阶段触发断言），可以使用Assert断言配合，但这不如pragma Unreachable;直接：

function Linear_Search (A : Elem_Array; E : Elem) return Index is
begin
   for i in A'Range loop
      pragma Loop_Invariant (for some J in i .. A'Last => A (J) = E);
      if A (i) = E then
         return i;
      end if;
   end loop;
   pragma Assert (False, "Linear_Search reached unreachable code: element not found");
   pragma Unreachable; -- 仍需配合Unreachable让编译器优化
end Linear_Search;

注意事项： #

• 不能直接移除循环后的返回语句：Ada要求函数的所有控制路径都必须有明确的返回值，即使逻辑上不可达，编译器也会报错。pragma Unreachable;是唯一能替代返回语句、同时让编译器接受的方式——它告诉编译器不需要此处的返回逻辑，因为永远不会走到这里。

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