4

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 仍然无法证明缺少别名。为什么这个前提条件不充分？

4

1 回答 1

2

Swap如评论中所述，可以通过从包规范中删除子程序来减轻潜在别名的警告。然而，前提条件I /= JonSwap_Indexes然后也可以省略而不改变结果。此外，Swap2 (A, B : in out Positive)在包规范中再次添加一个只调用Swap包主体中的 now local 的新子程序不会导致潜在别名的警告再次出现。这表明问题实际上是对 的调用Swap，而不是可见性。

查看 GNATprove 的输出（即有关检查证明的信息），似乎Swap从包规范中删除会导致GNAT 编译器（前端）内联Swap到Swap_Indexes. 内联有效地删除了对Swapfrom的调用，Swap_Indexes并因此有理由警告由于混叠导致的潜在影响。

注意：这实际上可以通过将调试选项传递-gnatd.j给编译器（参见此处）并将选项传递--no-inlining给 GNATprove 来验证，如下例所示。

因此，对于特定示例，虽然可以通过从包规范中删除来减轻别名警告Swap，但该解决方案并未回答为什么前提条件I /= J不能证明不存在别名的原始问题。虽然我不能肯定地说，但我怀疑这只是 GNATprove 证明非静态实际参数不存在别名的能力的当前限制。因此请注意，虽然在示例中的前提条件下没有混叠效应是显而易见的，但总体上证明这一点可能很快变得（非常）困难。

广告

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;

输出（GNATprove）

$ 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.

输出（GNATprove）

$ 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
于 2020-12-02T18:23:37.347 回答