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

I have the following code:

   function Linear_Search (A : Elem_Array; E : Elem) return Index is
   begin
      for i in A'Range loop
         pragma Loop_Invariant (for some J in i .. A'Last => A (J) = E);
         if A (i) = E then
            return i;
         end if;
      end loop;
      return A'Last;
   end Linear_Search;

This function has a precondition that says that the array contains the element searched for:

   function Contains (A : Elem_Array; E : Elem) return Boolean is
     (for some I in A'Range => A (I) = E);

   function Linear_Search (A : Elem_Array; E : Elem) return Index with
      Pre  => Contains (A, E),
      Post => A (Linear_Search'Result) = E;

So I would like to remove the return statement after the loop, or at least mark it as unreachable for clarity; is there any way to do that such that the compiler can also use that to optimize? What is the recommended way to mark unreachable code in Ada/SPARK?

Suppose I have a subprogram written using the SPARK Ada subset with postconditions verifying some property - for example, that the returned array is sorted, whose body just calls out to a function external to SPARK - for example, a C/C++ function that sorts arrays. Is there any way to force SPARK to assume, after this call, that the array will be sorted?