Проверка диапазона и длины в Аде (режим SPARK)

Ваша программа продолжает добавлять большую часть строки к вашему результату. Это делает строку намного больше, чем исходный строковый параметр. Вы не можете исправить это с помощью улучшенных предварительных условий или условий публикации.

Посмотрите разницу между вашим решением и функцией 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 продолжает увеличивать индекс входной строки и конкатенировать этот символ в конце всех символов, которые еще предстоит реверсировать. Предложение else в Reverse_String добавляет пустую строку к последнему символу, чтобы компилятор рассматривал ее как строку, а не как символ, потому что 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;   

У 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;

С небольшим изменением вы также можете обрабатывать строки нулевой длины.

Во многих случаях 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) );

(Подсказка: «Ада» — это женское имя, а не аббревиатура. GNATProve — это инструмент статического анализа, а не компилятор.)