Ada SPARK中字符串转整数的SPARK Prove前置条件失败问题求助

我来帮你分析一下这个问题：SPARK Prove提示precondition might fail，是因为它无法确认你调用Integer'Value时满足所有前置条件——哪怕你写了字符检查函数，SPARK也不知道这个函数能覆盖Integer'Value的全部前置要求。

为什么你的检查函数没用？ #

Integer'Value的前置条件远不止"仅包含数字字符"，它还要求：

• 字符串不能为空
• 转换后的数值必须落在Integer的取值范围内（不能大于Integer'Last或小于Integer'First）
• 如果是负数，开头只能有一个'-'（如果你的场景允许负数的话）

你的现有检查函数只覆盖了字符检查，没处理范围和空串，更关键的是：你没告诉SPARK Prover"当我的检查函数返回True时，Integer'Value的前置条件都满足"。

解决方案：给检查函数加上SPARK合约 #

我们需要写一个带**SPARK合约（Contract）**的检查函数，明确它和Integer'Value前置条件的关联，同时覆盖所有必要的检查逻辑。

1. 编写带范围检查的验证函数

下面是针对正整数场景的实现（如果需要支持负数，可以调整逻辑）：

function Is_Valid_Positive_Integer_Str(S : Unbounded_String) return Boolean is
   Str : constant String := To_String(S);
   -- 获取Integer'Last的字符串长度（去掉默认Image输出的前导空格）
   Max_Length : constant Natural := Integer'Image(Integer'Last)'Length - 1;
   -- 用更大的类型计算，避免溢出
   Current_Value : Long_Long_Integer := 0;
begin
   -- 检查空串
   if Str'Length = 0 then
      return False;
   end if;
   -- 长度超过Integer'Last的字符串直接无效
   if Str'Length > Max_Length then
      return False;
   end if;
   -- 检查每个字符都是数字，并逐位计算数值判断是否超出范围
   for C of Str loop
      if C not in '0' .. '9' then
         return False;
      end if;
      Current_Value := Current_Value * 10 + Character'Pos(C) - Character'Pos('0');
      if Current_Value > Long_Long_Integer(Integer'Last) then
         return False;
      end if;
   end loop;
   return True;
end Is_Valid_Positive_Integer_Str;

2. 添加SPARK合约关联前置条件

给函数加上合约，告诉SPARK Prover：当函数返回True时，Integer'Value的所有前置条件都满足：

function Is_Valid_Positive_Integer_Str(S : Unbounded_String) return Boolean with
   Post => (if Is_Valid_Positive_Integer_Str'Result then
               -- 非空
               To_String(S)'Length > 0 and then
               -- 全是数字字符
               (for all C of To_String(S) => C in '0' .. '9') and then
               -- 数值在Integer范围内
               Integer'Value(To_String(S)) <= Integer'Last);

3. 在主程序中安全调用Integer'Value

现在你可以在主程序中先调用检查函数，确保只有通过验证时才转换：

with Ada.Strings.Unbounded; use Ada.Strings.Unbounded;
procedure Main is
pragma SPARK_Mode;
   function Is_Valid_Positive_Integer_Str(S : Unbounded_String) return Boolean is
      Str : constant String := To_String(S);
      Max_Length : constant Natural := Integer'Image(Integer'Last)'Length - 1;
      Current_Value : Long_Long_Integer := 0;
   begin
      if Str'Length = 0 then
         return False;
      end if;
      if Str'Length > Max_Length then
         return False;
      end if;
      for C of Str loop
         if C not in '0' .. '9' then
            return False;
         end if;
         Current_Value := Current_Value * 10 + Character'Pos(C) - Character'Pos('0');
         if Current_Value > Long_Long_Integer(Integer'Last) then
            return False;
         end if;
      end loop;
      return True;
   end Is_Valid_Positive_Integer_Str;
   
   function Is_Valid_Positive_Integer_Str(S : Unbounded_String) return Boolean with
      Post => (if Is_Valid_Positive_Integer_Str'Result then
                  To_String(S)'Length > 0 and then
                  (for all C of To_String(S) => C in '0' .. '9') and then
                  Integer'Value(To_String(S)) <= Integer'Last);

   test_string : Unbounded_String;
   identifier : Integer;
begin
   test_string := To_Unbounded_String("1");
   -- 先验证再转换
   if Is_Valid_Positive_Integer_Str(test_string) then
      identifier := Integer'Value(To_String(test_string));
   else
      -- 处理无效输入的逻辑（比如设置默认值或抛出异常）
      identifier := 0;
   end if;
end Main;

额外提示 #

• 如果需要支持负数，修改检查函数允许开头的一个'-'，并添加对Integer'First的范围检查。
• 如果你的输入是确定有效的（比如测试用例），可以用pragma Assert(Is_Valid_Positive_Integer_Str(test_string));替代if语句，直接告诉Prover输入合法。

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