如何让GNATprove认可对同一输入两次调用Integer'Value结果一致？

问题场景 #

当两次调用Integer'Value解析同一个合法整数字符串时，GNATprove无法自动证明两次解析结果相等，导致断言X1 = X2被标记为"might fail"。

代码示例 #

主程序 Eq_Test.adb #

with String_Problem;

procedure Eq_Test is
begin
   String_Problem.String_Equal("4456");
end Eq_Test;

包规范 String_Problem.ads #

package String_Problem
with Spark_Mode
is
   procedure String_Equal
     (A : String)
   with
       Ghost;
end String_Problem;

包体 String_Problem.adb #

package body String_Problem
with Spark_Mode
is
   procedure String_Equal
     (A : String)
   is
      X1 : Integer;
      X2 : Integer;
   begin
      X1 := Integer'Value (A);
      pragma Annotate
        (Gnatprove, False_Positive, "precondition might fail", "we only call on valid integer strings");
      X2 := Integer'Value (A);
      pragma Annotate
        (Gnatprove, False_Positive, "precondition might fail", "we only call on valid integer strings");
      pragma Assert (X1 = X2);
   end String_Equal;
end String_Problem;

GNATprove 输出 #

alr gnatprove
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...

string_problem.adb:16:22: medium: assertion might fail
   16 |      pragma Assert (X1 = X2);
      |                     ^~~~~~~
Summary logged in [path]/gnatprove/gnatprove.out

解决方案 #

1. 为过程添加前置条件约束输入合法性 #

修改String_Problem.ads，给String_Equal添加前置条件，明确输入字符串是合法的整数字符串。这不仅能消除Integer'Value前置条件的警告，还能让GNATprove明确输入的有效性，为后续的确定性证明提供基础：

package String_Problem
with Spark_Mode
is
   procedure String_Equal
     (A : String)
   with
       Ghost,
       Pre => Integer'Wide_Value_String(A); -- 确保输入是合法整数字符串
end String_Problem;

2. 移除不必要的False_Positive注解 #

修改String_Problem.adb，去掉针对Integer'Value的False_Positive注解，因为前置条件已经保证了输入符合Integer'Value的调用要求：

package body String_Problem
with Spark_Mode
is
   procedure String_Equal
     (A : String)
   is
      X1 : Integer;
      X2 : Integer;
   begin
      X1 := Integer'Value (A);
      X2 := Integer'Value (A);
      pragma Assert (X1 = X2);
   end String_Equal;
end String_Problem;

3. 验证证明结果 #

重新运行alr gnatprove，此时GNATprove会利用Integer'Value的纯函数特性（相同输入必然返回相同结果），结合前置条件的约束，成功证明X1 = X2的断言成立，不会再出现断言可能失败的警告。

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