交换数组索引 SPARK-Ada 中潜在的别名冲突

Question

Spark 简介课程包含一个示例 (#5)，其中 GNATprove 无法证明交换数组的两个元素的过程中不会出现别名：

package P
  with SPARK_Mode => On
is
   type P_Array is array (Natural range <>) of Positive;

   procedure Swap_Indexes (A : in out P_Array; I, J : Natural);
   procedure Swap (X, Y : in out Positive);
end P;

package body P
  with SPARK_Mode => On
is
   procedure Swap (X, Y : in out Positive) is
      Tmp : constant Positive := X;
   begin
      X := Y;
      Y := Tmp;
   end Swap;

   procedure Swap_Indexes (A : in out P_Array; I, J : Natural) is
   begin
      Swap (A (I), A (J));
   end Swap_Indexes;

end P;

GNATprove 说

p.adb:13:13: medium: formal parameters "X" and "Y" might be aliased (SPARK RM 6.4.2)

。这似乎是一个有效的错误，因为传递给

Swap_Indexes

的索引可能是相等的。然而，在

Pre => I /= J

中添加前提条件

Swap_Indexes

后，GNATprove仍然无法证明不存在混叠。为什么这个前提条件不充分？

Answer 1

如评论中所述，可以通过从包规范中删除

Swap

子程序来减轻潜在别名的警告。然而，也可以省略

I /= J

上的前提

Swap_Indexes

，而不会改变结果。此外，在包规范中再次添加一个新的

Swap2 (A, B : in out Positive)

子程序，仅调用包主体中现在本地的

Swap

，不会导致重新出现潜在别名的警告。这表明问题实际上是对

Swap

的调用，而不是它的可见性。

查看 GNATprove 的输出（即已证明的检查信息），似乎从包规范中删除

Swap

会导致 GNAT 编译器（前端）将

Swap

内联到

Swap_Indexes

中。内联有效地从

Swap

中删除了对

Swap_Indexes

的调用，并因此有理由警告由于混叠而造成的潜在影响。

注意：这实际上可以通过将调试选项

-gnatd.j

传递给编译器（参见 here）并将选项

--no-inlining

传递给 GNATprove 来验证，如下例所示。

因此，对于特定示例，虽然可以通过从包规范中删除

Swap

来缓解有关别名的警告，但该解决方案并没有回答为什么前提条件

I /= J

无法证明不存在别名的原始问题。虽然我不能肯定地说，但我怀疑这只是 GNATprove 证明非静态实际参数不存在别名的能力的当前限制。从而注意到，虽然考虑到示例中的前提条件，明显不存在混叠效应，但一般来说证明这一点可能很快就会变得（非常）困难。

p.广告

package P with SPARK_Mode is

   type P_Array is array (Natural range <>) of Positive;

   procedure Swap_Indexes (A : in out P_Array; I, J : Natural)
     with Pre => I in A'Range and J in A'Range;
   
   procedure Swap2 (A, B : in out Positive)
     with Global => null;
   
end P;

p.adb

package body P with SPARK_Mode is
   
   procedure Swap (X, Y : in out Positive) is
      Tmp : constant Positive := X;
   begin
      X := Y;
      Y := Tmp;
   end Swap_Local;
   
   procedure Swap_Indexes (A : in out P_Array; I, J : Natural) is
   begin
      Swap (A (I), A (J));
   end Swap_Indexes;
   
   procedure Swap2 (A, B : in out Positive) is
   begin
      Swap (A, B);
   end Swap2;

end P;

输出（GNAT证明）

$ gnatprove -Pdefault.gpr -j0 --level=1 --report=all -cargs -gnatd.j
Phase 1 of 2: generation of Global contracts ...
List of calls inlined by the frontend
  1:p.adb:12:7:
  2:p.adb:17:7:
Phase 2 of 2: flow analysis and proof ...
List of calls inlined by the frontend
  1:p.adb:12:7:
  2:p.adb:17:7:
p.adb:4:34: info: index check proved, in call inlined at p.adb:12
p.adb:6:07: info: index check proved, in call inlined at p.adb:12
p.adb:6:12: info: index check proved, in call inlined at p.adb:12
p.adb:7:07: info: index check proved, in call inlined at p.adb:12
p.ads:9:11: info: data dependencies proved
Summary logged in [...]/gnatprove.out

请求 GNATprove 不要内联 (

--no-inlining

) 会使警告重新出现，即使前提条件

I /= J

添加到

Swap_Indexes

。

输出（GNAT证明）

$ gnatprove --no-inlining -Pdefault.gpr -j0 --level=1 --report=all -cargs -gnatd.j
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
p.adb:12:13: medium: formal parameters "X" and "Y" might be aliased (SPARK RM 6.4.2)
p.adb:12:16: info: index check proved
p.adb:12:23: info: index check proved
p.ads:9:11: info: data dependencies proved
Summary logged in [...]/gnatprove.out