2

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.

Jacob Sparre Andersen
  • 6,733
  • 17
  • 22
LT 'syreal' Jones
  • 97
  • 1
  • 9
  • 1
    The challenge with loop invariants is that they have to be provable both from entry into the loop to the loop invariant, and from the loop invariant, through one loop iteration and back to the loop invariant again. Can you do that by hand with your current loop invariants? – Jacob Sparre Andersen Nov 12 '17 at 14:02
  • Thanks, that's a good way to visualize what's needed to prove a loop invariant. I can't prove my above loop invariants, and I suppose that's because they're wrong, X*Y isn't the count of the current iteration. I would expect the first iteration to be provable, but after the first iteration not to be provable, but it's exactly opposite of that. – LT 'syreal' Jones Nov 13 '17 at 19:57

1 Answers1

3

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.

Jacob Sparre Andersen
  • 6,733
  • 17
  • 22