these last weeks I have been trying to learn the ADA language, to do it I made an exercise to reverse a string using recursion, however when I compile it with GNATProve it gives me several errors which I have not been able to solve, it would be of great help if you could guide me on how to solve them using Preconditions and Postconditions.
My code:
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;
Errors:
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
I'm tried using Preconditons and Postconditions about the input Str length