如何证明嵌入在双循环中的函数的 Ada/SPARK 前提条件

Question

我试图证明 "prepend" 的先决条件在下面程序的执行过程中成立。前提是：

Length (Container) < Container.Capacity

我在下面的代码中以 pragmas 的形式尝试证明这一点。我可以证明这个先决条件适用于单循环但不适用于双循环。我找不到任何双循环的例子，虽然我找到了非常复杂的循环不变量的例子。

规格：

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;

错误是"loop invariant might fail in first iteration, cannot prove 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;

请注意我是如何关注循环不变量中列表长度的演变。

如何证明嵌入在双循环中的函数的 Ada/SPARK 前提条件

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

ada

proofs

doubly-linked-list

spark-2014