SPARK中能否绕过契约/断言？如何让SPARK认可外部函数后置条件？

1. 让SPARK假设外部函数满足后置条件的方法 #

由于SPARK无法分析C/C++等外部函数的实现，你需要显式告知验证器该函数执行后的效果，常用方式有两种：

• 给外部函数添加契约并配合pragma Assume
  先为导入的外部函数声明契约，然后在调用它的SPARK子程序中，用pragma Assume确认外部函数满足契约要求。示例代码：

  package Sorter is
     type Integer_Array is array (Positive range <>) of Integer;
     function Is_Sorted (A : Integer_Array) return Boolean
       with Ghost; -- 幽灵函数，仅用于验证逻辑
  
     procedure C_Sort (A : in out Integer_Array)
       with Import, Convention => C; -- 导入外部C排序函数
  end Sorter;
  
  package body Sorter is
     function Is_Sorted (A : Integer_Array) return Boolean is
     begin
        if A'Length <= 1 then
           return True;
        end if;
        for I in A'First .. A'Last - 1 loop
           if A(I) > A(I+1) then
              return False;
           end if;
        end loop;
        return True;
     end Is_Sorted;
  
     procedure Sort (A : in out Integer_Array) is
     begin
        C_Sort (A);
        pragma Assume (Is_Sorted (A)); -- 告知SPARK：调用后数组已排序
     end Sort;
  end Sorter;
  

  这里的pragma Assume会让SPARK验证器直接接受Is_Sorted(A)为真，无需自动证明。

• 为外部函数添加契约并使用公理（Axiom）
  你也可以在包的规范中用公理陈述外部函数的行为，这样所有调用该函数的地方都会自动继承这个假设：

  package Sorter is
     -- 省略类型和Is_Sorted函数声明
     procedure C_Sort (A : in out Integer_Array)
       with Import, Convention => C;
  
     axiom C_Sort_Ensures_Sorted :
       for all A : Integer_Array =>
         (declare
             Temp : Integer_Array := A;
          begin
             C_Sort (Temp);
             Is_Sorted (Temp)
          end);
  end Sorter;
  

  注意公理的编写必须严谨，错误的公理会导致验证结果完全不可靠。

2. 在SPARK中绕过契约或断言的方式 #

SPARK提供了几种绕过契约/断言验证的机制，但这些操作都存在风险，仅应在你能手动确认条件绝对成立的场景下使用：

• pragma Assume：如上述示例，直接让验证器假设某个条件成立，属于局部绕过，影响范围仅限于当前代码位置。
• pragma Assertion_Policy：通过设置断言策略为Ignore，可以全局或针对特定单元禁用契约、断言的验证。例如：

  pragma Assertion_Policy (Post => Ignore); -- 禁用所有后置条件验证
  

  这种方式会关闭一类或所有断言检查，不推荐在生产代码中随意使用，仅适合临时调试或特殊场景。
• 幽灵代码的条件编译：如果断言写在幽灵代码中，可以通过编译选项-gnatX禁用幽灵代码，从而忽略这些断言，但这会同时移除所有用于验证的幽灵逻辑。

需要强调的是，绕过契约或断言会直接削弱SPARK的验证能力，可能引入未被发现的错误，使用时必须确保已手动验证相关条件的正确性。

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