How to prove a Ada/SPARK precondition on a function embedded in a double loop

Question

I'm trying to prove that the precondition of "prepend" holds during the execution of the program below. The precondition is:

Length (Container) < Container.Capacity

My attempts at proving this are in the code below in the form of pragmas. I can prove this precondition holds for a single loop but not for a double loop. I can't find any examples for double loops, though I've found examples of very complex loop invariants.

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;

Body:

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;

The error is "loop invariant might fail in first iteration, cannot prove Illumination_Sources_Pkg.Length(Illumination_Sources) <= X*Y" It doesn't say that it might fail after the first iteration, so that's something.

Answer 1

Choosing the limits (we separate the limits on the outer and inner loop, to make things clear):

package Double_Loop
  with SPARK_Mode
is

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

end Double_Loop;

We instantiate the generic package as a library level package:

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

Specification of the main program:

procedure Double_Loop.Run with SPARK_Mode;

And then the body of the main program:

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;

Notice how I've focused on the evolution in the length of the list in the loop invariants.