Как доказать предусловие Ada/SPARK для функции, встроенной в двойной цикл

Question

Я пытаюсь доказать, что предварительное условие "prepend" выполняется во время выполнения программы ниже. Предварительное условие:

Length (Container) < Container.Capacity

Мои попытки доказать это приведены в коде ниже в форме прагм. Я могу доказать, что это предварительное условие выполняется для одного цикла, но не для двойного цикла. Я не могу найти примеров для двойных циклов, хотя я нашел примеры очень сложных инвариантов цикла.

Spec:

with Ada.Containers.Formal_Doubly_Linked_Lists; use Ada.Containers;

package spec with SPARK_Mode is

   MAX_ILLUMINATION_SOURCES : constant Count_Type := 250001;

   package Illumination_Sources_Pkg is new 
Ada.Containers.Formal_Doubly_Linked_Lists
      (Element_Type => Positive);

   Illumination_Sources : 
Illumination_Sources_Pkg.List(MAX_ILLUMINATION_SOURCES);

end spec;

Тело:

with spec; use spec;
with Ada.Containers; use Ada.Containers;

procedure Main with SPARK_Mode
is
begin
   Illumination_Sources_Pkg.Clear(Illumination_Sources);

   for Y in 1 .. 500 loop
      pragma Loop_Invariant( Y <= 500 );
      for X in 1 .. 500 loop
         Illumination_Sources_Pkg.Prepend(Illumination_Sources, 17);

         pragma Loop_Invariant( X <= 500 and X*Y <= 500*500 and 
                             Illumination_Sources_Pkg.Length(Illumination_Sources) <= Count_Type(X*Y) and
                            Count_Type(X*Y) <     Illumination_Sources.Capacity);
      end loop;
   end loop;
end Main;

Ошибка: "Инвариант цикла может потерпеть неудачу в первой итерации, не может доказать Illumination_Sources_Pkg.Length(Illumination_Sources) <= X*Y" Это не говорит о том, что он может завершиться неудачей после первой итерации, так что это что-то.

Answer 1

Выбор пределов (мы разделяем ограничения на внешний и внутренний цикл, чтобы прояснить ситуацию):

package Double_Loop
  with SPARK_Mode
is

   Outer_Limit : constant := 500;
   Inner_Limit : constant := 500;

end Double_Loop;

Мы создаем экземпляр универсального пакета как пакет уровня библиотеки:

pragma SPARK_Mode;

with Ada.Containers.Formal_Doubly_Linked_Lists;

package Double_Loop.Lists is
  new Ada.Containers.Formal_Doubly_Linked_Lists (Element_Type => Positive);

Спецификация основной программы:

procedure Double_Loop.Run with SPARK_Mode;

А затем тело основной программы:

with Ada.Containers;

with Double_Loop.Lists;

procedure Double_Loop.Run with SPARK_Mode is
   use all type Ada.Containers.Count_Type;

   Data : Lists.List (Capacity => Outer_Limit * Inner_Limit);

begin
   Lists.Clear (Data);

   Outer :
   for Y in Ada.Containers.Count_Type range 1 .. Outer_Limit loop

      Inner :
      for X in Ada.Containers.Count_Type range 1 .. Inner_Limit loop
         Lists.Prepend (Container => Data,
                        New_Item  => 17);

         pragma Loop_Invariant
           (Lists.Length (Data) = (Y - 1) * Inner_Limit + X);
      end loop Inner;

      pragma Loop_Invariant (Lists.Length (Data) = Y * Inner_Limit);
   end loop Outer;
end Double_Loop.Run;

Обратите внимание, как я сфокусировался на эволюции длины списка в инвариантах цикла.