隐式函数契约不可用于证明

Question

我在 SPARK 包中有一个过程，它从非 SPARK 包中调用一些函数。

procedure do_monitoring is
   U_C1 : constant Float := Sim.Get_U_C1;
   I_L1 : constant Float := Sim.Get_I_L1;
   U_C2 : constant Float := Sim.Get_U_C2;
   I_L2 : constant Float := Sim.Get_I_L2;
begin
   pragma Assert (U_C1 in Float_Signed1000);
   pragma Assert (I_L1 in Float_Signed1000);
   pragma Assert (U_C2 in Float_Signed1000);
   pragma Assert (I_L2 in Float_Signed1000);
   --  Monitor PFC intermediate voltage
   monitor_signal (monitor_pfc_voltage, U_C1);
   --  Monitor PFC inductor current
   monitor_signal (monitor_pfc_current, I_L1);
   --  Monitor output voltage
   monitor_signal (monitor_output_voltage, U_C2);
   --  Monitor output inductor current
   monitor_signal (monitor_output_current, I_L2);
end do_monitoring;

GNAT 为我从全局受保护类型调用函数的所有四个声明行提供了 info: implicit function contract not available for proof (<function_name> may not return)。

受保护类型函数在非 SPARK 包中定义如下，并使用在受保护类型私有部分中声明的记录 Sim_Out。所有的记录值都用0.0初始化。

function Get_I_L1 return Float is
begin
   return Sim_Out.I_L1;
end Get_I_L1;

function Get_U_C1 return Float is
begin
   return Sim_Out.U_C1;
end Get_U_C1;

function Get_I_L2 return Float is
begin
   return Sim_Out.I_L2;
end Get_I_L2;

function Get_U_C2 return Float is
begin
   return Sim_Out.U_C2;
end Get_U_C2;

有什么办法可以解决这个问题？我确实已经添加了一些编译指示来为证明者提供额外的信息subtype Float_Signed1000 is Float range -1_000.0 .. 1_000.0，但这并没有达到我的预期。

我想在这里就这个话题提出你的建议。

Answer 1

如果允许我编辑 Sim 包，我可以说例如

package Sim
with SPARK_Mode
is
   function Get return Float
   with Annotate => (Gnatprove, Terminating);
end Sim;

（那是使用AdaCore的spark2017版本），后续使用非SPARK体

package body Sim is
   function Get return Float is (42.0);
end Sim;

报告显示 Sim.Get 已被跳过。

我不知道 SPARK2014 的后续版本对此有何反应，因为 User Guide 的含义是 Annotate 为证明者设定了一个目标，但我们不允许它调查Sim 的正文进行检查。

参考手册中可能还有更多内容 - 访问 adacore.com，选择 Resources/Documentation/SPARK。