2

我试图证明“前置”的前提条件在执行下面的程序期间成立。前提是：

Length (Container) < Container.Capacity

我在下面的代码中以 pragma 的形式尝试证明这一点。我可以证明这个前提条件适用于单循环，但不适用于双循环。尽管我找到了非常复杂的循环不变量的示例，但我找不到任何双循环示例。

规格：

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” 它并没有说它可能在第一次迭代后失败，所以这就是问题。

4

1 回答 1

3

选择限制（我们将外部和内部循环的限制分开，以使事情清楚）：

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;

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

于 2017-11-12T15:09:53.733 回答