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