ada - (Ada) SPARK 中的冰点问题

Question

我有以下包:

-------------------
-- File: father.ads
-------------------

package Father with SPARK_Mode => On is

   pragma Elaborate_Body;
   
   type Father_T is abstract tagged private;
   
   function Get_Field_1 (Self : Father_T) return Positive;
   
   procedure Proc_1 (Self : in out Father_T; Another : Father_T) is abstract;
   
   function Func_1 (Self : Father_T) return Boolean is abstract;
   
private

   pragma SPARK_Mode (Off);
   
   type Father_T is abstract tagged record
      
      Field_1 : Positive := 1;
      
   end record;
   
end Father;

--------------------------
-- File: father-middle.ads
--------------------------

package Father.Middle with SPARK_Mode => On is

   pragma Elaborate_Body;
   
   type Middle_T is abstract new Father_T with null record; -- [L1]

   overriding procedure Proc_1 (Self : in out Middle_T; Another : Middle_T);
   
private
   
   pragma SPARK_Mode (Off);
   
   function Func_2 (Self : Middle_T) return Boolean;
   
end Father.Middle; -- [L3]

--------------------------
-- File: father-middle.adb
--------------------------

package body Father.Middle is

   ------------
   -- Proc_1 --
   ------------

   overriding procedure Proc_1 (Self : in out Middle_T; Another : Middle_T) is -- [L2]
   begin
      Self.Field_1 := Self.Field_1 + Another.Field_1;
   end Proc_1;

   ------------
   -- Func_2 --
   ------------

   function Func_2 (Self : Middle_T) return Boolean is
   begin
      return False;
   end Func_2;

end Father.Middle;

-------------------------------
-- File: father-middle-lead.ads
-------------------------------

package Father.Middle.Leaf with SPARK_Mode => On is

   pragma Elaborate_Body;
   
   type Leaf_T is new Middle_T with null record;
   
   function Create return Leaf_T;
   
   overriding function Func_1 (Self : Leaf_T) return Boolean;

end Father.Middle.Leaf;

编译器报如下错误:

father-middle.ads:7:04:类型“Middle_T”的第一个凝固点必须出现在原始体“Proc_1”的早期调用区域内 (SPARK RM 7.7(8)) [L1]

father-middle.ads:7:04:区域从 father-middle.adb:7 [L2] 开始

father-middle.ads:7:04:区域结束于 father-middle.adb:7 [L2]

father-middle.ads:7:04: 第17行第一个冰点[L3]

如果我在 Father.Middle.Leaf 而不是 Father.Middle 中覆盖 Proc_1，错误就消失了。

我已阅读 https://docs.adacore.com/spark2014-docs/html/lrm/packages.html#elaboration-issues但我是 SPARK 的新手。

有没有办法覆盖 Father.Middle 中的 Proc_1？

我在 Windows 10 中使用 GNAT Studio Community 2020。

Answer 1

不幸的是，我没有一个决定性的答案，但我确实怀疑早期的区域分析在这里是否真的正确。

我怀疑的原因是，如果你添加一个新的具体类型 Dummy_T 到继承自 Middle_T 的 Father.Middle 然后突然所有看起来不错(如下所示)。在我看来(但我在这里可能是错的)添加这样的类型不应该改变 Middle_T 的 Proc_1 的早期区域分析的结果；唯一的区别是 Middle_T 的卡住点从原始代码中的 package spec 末尾移到了下面代码中 Dummy_T 的类型定义之前。

此外，还不清楚为什么 Father.Middle 主体中 Proc_1 的早期区域没有扩展到包规范中，因为 pragma Elaborate_Body 已在 Father.Middle 中说明。看起来(如果我理解 SPARK RM 7.7(4) and 7.7(9) 正确的话)早期区域分析器在正文的开头或 Father.Middle 的规范结尾的某处检测到一个不可预先构建的构造。但是，似乎没有这样的东西。所以也许在扩展代码的分析中出了问题，但这纯粹是猜测，因为早期的区域分析器没有提供任何 debugging facilities。来追踪它的行为。因此，很难从最终用户的角度检查分析器的推理。

请再次注意，我作为一名最终用户的分析是假设性的。错误可能仍然是正确的，我可能是错的。我只是觉得我的发现很有趣，值得分享。

(GNAT 引用:error，分析器spec 和main routine)

father-middle.ads

package Father.Middle with SPARK_Mode is
   pragma Elaborate_Body;
   
   type Middle_T is abstract new Father_T with null record;

   overriding procedure Proc_1 (Self : in out Middle_T; Another : Middle_T);
   
private
   pragma SPARK_Mode (Off);
   
   function Func_2 (Self : Middle_T) return Boolean;
   
   --
   --  ??? Just add a new concrete type and all is fine now?
   --
   
   type Dummy_T is new Middle_T with null record;
   
   overriding function Func_1 (Self : Dummy_T) return Boolean is (False);
   
end Father.Middle;