ada - Ada 中的范围检查和长度检查(SPARK 模式)

Question

最近几周我一直在尝试学习 ADA 语言，为此我做了一个使用递归反转字符串的练习，但是当我用 GNATProve 编译它时，它给了我几个我无法解决的错误，如果您能指导我如何使用先决条件和后置条件来解决它们，那将会有很大的帮助。

我的代码:

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: low: range check might fail
   18>|                   String_Reverse (Str (Str'First + 1 .. Str'Last)) &
   19 |                   Str (Str'First);
  reason for check: result of concatenation must fit in the target type of the assignment
  possible fix: precondition of subprogram at line 8 should mention Str
    8 |      function String_Reverse(Str:String) return String with
      |      ^ here
dth113.adb:18:69: medium: length check might fail
   18>|                   String_Reverse (Str (Str'First + 1 .. Str'Last)) &
   19 |                   Str (Str'First);
  reason for check: array must be of the appropriate length
  possible fix: precondition of subprogram at line 8 should mention Str
    8 |      function String_Reverse(Str:String) return String with
      |      ^ here

我尝试使用关于输入 Str 长度的先决条件和后置条件

Answer 1

Gnatprove 在连接数组方面似乎存在一些困难。

下面使用子类型而不是前置条件和后置条件证明了这一点。证明结果实际上是输入字符串的反转可能会更棘手!

规范:

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

正文:

pragma SPARK_Mode;
function String_Reverse (Str : String) return String is
   subtype Result_String is String (Str'Range);
   Result : Result_String;
begin
   if Str'Length = 1 then
      Result := Str;
   else
      declare
         subtype Part_String is String (1 .. Str'Length - 1);
         Reversed_Part : constant Part_String
           := String_Reverse (Str (Str'First + 1 .. Str'Last));
      begin
         Result := Reversed_Part & Str (Str'First);
      end;
   end if;
   return Result;
end String_Reverse;

---

只需稍加更改，您也可以处理零长度字符串。