Ada（SPARK模式）递归字符串反转的范围与长度检查错误修复

最近学习Ada时编写了一个递归实现字符串反转的函数，但使用GNATProve编译时触发了范围检查和长度检查错误。已尝试为输入Str的长度设置前置和后置条件，但问题仍未解决，需要指导如何通过调整前置/后置条件修复这些错误。

我的代码 #

function String_Reverse(Str:String) return String with
        Pre => Str'Length > 0 ,
        Post => String_Reverse'Result'Length <= Str'Length;
        function String_Reverse (Str : String) return String is
            Result : String (Str'Range);
        begin
            if Str'Length = 1 then
                Result := Str;
            else
                Result :=
                   String_Reverse (Str (Str'First + 1 .. Str'Last)) &
                   Str (Str'First);
         end if;
            return Result;
        end String_Reverse;

错误信息 #

dth113.adb:18:69: 低级：范围检查可能失败
   18>|                   String_Reverse (Str (Str'First + 1 .. Str'Last)) &
   19 |                   Str (Str'First);
  检查原因：拼接结果必须适配赋值目标类型
  可能的修复：第8行子程序的前置条件应提及Str
    8 |      function String_Reverse(Str:String) return String with
      |      ^ 此处
dth113.adb:18:69: 中级：长度检查可能失败
   18>|                   String_Reverse (Str (Str'First + 1 .. Str'Last)) &
   19 |                   Str (Str'First);
  检查原因：数组必须具备合适的长度
  可能的修复：第8行子程序的前置条件应提及Str
    8 |      function String_Reverse(Str:String) return String with
      |      ^ 此处

修复方案 #

问题核心在于当前的后置条件约束过弱，无法让GNATProve推导出拼接结果的长度完全匹配Result的范围。

调整后置条件 #

将原后置条件String_Reverse'Result'Length <= Str'Length改为严格相等：

Post => String_Reverse'Result'Length = Str'Length;

修改后的完整代码 #

function String_Reverse(Str: String) return String with
    Pre => Str'Length > 0,
    Post => String_Reverse'Result'Length = Str'Length;

function String_Reverse (Str : String) return String is
    Result : String (Str'Range);
begin
    if Str'Length = 1 then
        Result := Str;
    else
        Result :=
           String_Reverse (Str (Str'First + 1 .. Str'Last)) &
           Str (Str'First);
    end if;
    return Result;
end String_Reverse;

修复原理 #

1. Result的声明范围是Str'Range，其长度必然等于Str'Length
2. 递归调用String_Reverse(Str(Str'First+1..Str'Last))的子串长度为Str'Length - 1，调整后置条件后，GNATProve可证明该调用的返回结果长度等于子串长度
3. 子串反转结果拼接单个字符后，总长度为(Str'Length - 1) + 1 = Str'Length，完全匹配Result的长度，从而消除范围和长度检查错误

可选优化：支持空字符串 #

若需要处理空字符串，可移除前置条件并在代码中添加空字符串分支，后置条件保持不变：

function String_Reverse(Str: String) return String with
    Post => String_Reverse'Result'Length = Str'Length;

function String_Reverse (Str : String) return String is
    Result : String (Str'Range);
begin
    if Str'Length = 0 then
        return "";
    elsif Str'Length = 1 then
        Result := Str;
    else
        Result :=
           String_Reverse (Str (Str'First + 1 .. Str'Last)) &
           Str (Str'First);
    end if;
    return Result;
end String_Reverse;

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