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

在过去的几周里，我一直在尝试学习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长度的Preconditions和Postconditions

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;

只要做一个小改动，您也可以处理零长度的字符串。

您的程序不断将大部分字符串追加到结果中。这使得字符串比初始字符串参数大得多。您无法通过改进先决条件或后期条件来解决此问题。

查看您的解决方案与下面显示的Reverse_String函数之间的区别。在下面的解决方案中，返回字符串的大小不能是参数中函数字符串的大小，因为它正在用每次递归构建反向字符串，并且在所有递归完成之前无法确定字符串的大小。

with Ada.Text_IO; use Ada.Text_IO;
procedure Main is
function Reverse_String(S : in String; Idx : Positive) return String is
begin
if Idx < S'Last then
return Reverse_String(S, Idx + 1) & S(Idx);
else
return S(Idx) & "";
end if;
end Reverse_String;
S1 : String := "Hello World";
s2 : String := "1234567890";
N1 : Integer := 12345;
N3 : Integer;
begin
Put_Line(S1 & " : " & Reverse_String(S1, 1));
Put_Line(S2 & " : " & Reverse_String(S2, 1));
N3 := Integer'Value(Reverse_String(N1'Image, 1));
Put_Line(N1'Image & " : " & N3'Image);
end Main;

此版本的Reverse_String不断增加输入字符串的索引，并将该字符连接到所有尚未反转的字符的末尾。Reverse_String的else子句在最后一个字符后面附加一个空字符串，以便编译器将其视为字符串而非字符，因为s(Idx(是单个字符，不是字符串，但将s(Idx(与空字符串连接会产生字符串。

这里是另一个实现

function String_Reverse (Str : String) return String is
Result : String (Str'Range) := Str;
begin       
for I in reverse Str'Range loop
Result(Str'Last - I + Result'First) := Str(I);
end loop;
return Result;
end String_Reverse;

SPARK在很多情况下似乎更喜欢使用表达式函数而不是正则函数。我不知道这是否会有所不同，但你可以尝试将函数体重写为

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

(我希望括号平衡了。(

通常情况下，一个函数允许空字符串，并且该函数类似于

function Reversed (S : in String) return String with
Post => Reversed'Result'Length = S'Length;
function Reversed (S : in String) return String is
(if S'Length = 0 then ""
else Reversed (S (S'first + 1 .. S'Last) & S (S'First) );

(提示："Ada"是一个女人的名字，而不是缩写。GNATProve是一个静态分析工具，而不是编译器。(

相关内容

最新更新

热门标签：