1

我目前正在大学实时编程语言课程中学习 Ada，并且有一个关于 SPARK 的问题。

我正在从事一个项目，其任务是监控离网电源。这项任务对机器安全至关重要，因此应尽可能避免错误，例如用 SPARK 证明。我能够在 stackoverflow 上解决一些其他问题，但我仍然遇到无法通过用户指南中的快速搜索修复的错误。

错误是call to a volatile function in interfering context is not allowed in SPARK参考中的if monitoring_interface.is_all_config_set then ...行

task body monitoring_task is
      next_time : Time;
   begin
      --  Initialisation of next execution time
      next_time := Clock;
      --  Superloop
      loop
         Put_Line ("Run task monitoring");
         --  Load monitor configuration
         monitor_pfc_voltage.config := monitoring_interface.get_monitor_pfc_voltage_config;
         monitor_pfc_current.config := monitoring_interface.get_monitor_pfc_current_config;
         monitor_output_voltage.config := monitoring_interface.get_monitor_output_voltage_config;
         monitor_output_current.config := monitoring_interface.get_monitor_output_current_config;

         --  Check if module has been configured correctly
         --  Don't do anything otherwise
         if monitoring_interface.is_all_config_set then --  <= erroneous line
            do_monitoring;
         end if;

         next_time := next_time + TASK_PERIOD;
         delay until next_time;
      end loop;
   end monitoring_task;

该函数is_all_config_set在我用于任务间通信的受保护类型中定义。

package PSU_Monitoring is

   ... Declaration of some types (Monitor_Config_T) ...

   protected type Monitoring_Interface_T is
      function is_all_config_set return Boolean;

      procedure set_monitor_pfc_voltage_config (new_monitor_config : in Monitor_Config_T);
      function get_monitor_pfc_voltage_config return Monitor_Config_T;

      procedure set_monitor_pfc_current_config (new_monitor_config : in Monitor_Config_T);
      function get_monitor_pfc_current_config return Monitor_Config_T;

      procedure set_monitor_output_voltage_config (new_monitor_config : in Monitor_Config_T);
      function get_monitor_output_voltage_config return Monitor_Config_T;

      procedure set_monitor_output_current_config (new_monitor_config : in Monitor_Config_T);
      function get_monitor_output_current_config return Monitor_Config_T; 
   private
      --  Configuration for PFC intermediate voltage
      monitor_pfc_voltage_config : Monitor_Config_T;
      monitor_pfc_voltage_config_set : Boolean := False;
      --  Configuration for PFC inductor current
      monitor_pfc_current_config : Monitor_Config_T;
      monitor_pfc_current_config_set : Boolean := False;
      --  Configuration for output voltage
      monitor_output_voltage_config : Monitor_Config_T;
      monitor_output_voltage_config_set : Boolean := False;
      --  Configuration for output inductor current
      monitor_output_current_config : Monitor_Config_T;
      monitor_output_current_config_set : Boolean := False;
   end Monitoring_Interface_T;

   monitoring_interface : Monitoring_Interface_T;

private

... Declaration of a task and some private constants and subprograms ...

end PSU_Monitoring

相应的身体是

package body PSU_Monitoring is

   protected body Monitoring_Interface_T is

      function is_all_config_set return Boolean is
      begin
         return monitor_pfc_voltage_config_set and monitor_pfc_current_config_set and monitor_output_voltage_config_set and monitor_output_current_config_set;
      end is_all_config_set;

      procedure set_monitor_pfc_voltage_config (new_monitor_config : in Monitor_Config_T) is
      begin
         monitor_pfc_voltage_config := new_monitor_config;
         monitor_pfc_voltage_config_set := True;
      end set_monitor_pfc_voltage_config;

      function get_monitor_pfc_voltage_config return Monitor_Config_T is
      begin
         return monitor_pfc_voltage_config;
      end get_monitor_pfc_voltage_config;

      procedure set_monitor_pfc_current_config (new_monitor_config : in Monitor_Config_T) is
      begin
         monitor_pfc_current_config := new_monitor_config;
         monitor_pfc_current_config_set := True;
      end set_monitor_pfc_current_config;

      function get_monitor_pfc_current_config return Monitor_Config_T is
      begin
         return monitor_pfc_current_config;
      end get_monitor_pfc_current_config;

      procedure set_monitor_output_voltage_config (new_monitor_config : in Monitor_Config_T) is
      begin
         monitor_output_voltage_config := new_monitor_config;
         monitor_output_voltage_config_set := True;
      end set_monitor_output_voltage_config;

      function get_monitor_output_voltage_config return Monitor_Config_T is
      begin
         return monitor_output_voltage_config;
      end get_monitor_output_voltage_config;

      procedure set_monitor_output_current_config (new_monitor_config : in Monitor_Config_T) is
      begin
         monitor_output_current_config := new_monitor_config;
         monitor_output_current_config_set := True;
      end set_monitor_output_current_config;

      function get_monitor_output_current_config return Monitor_Config_T is
      begin
         return monitor_output_current_config;
      end get_monitor_output_current_config;

   end Monitoring_Interface_T;

... Definition of the remaining subprograms defined in the specification file ...

end PSU_Monitoring;

这里有什么问题？

4

1 回答 1

4

正如 Jeffrey 所说，我们需要查看程序中标记错误的部分。一般来说，这与具有副作用的功能有关，请参阅参考手册： http ://docs.adacore.com/spark2014-docs/html/lrm/packages.html#external-state-variables

如果您以“错误”的方式使用 Real-Time 包中的 Clock 函数，则会观察到相同的错误消息：

with Ada.Real_Time; use Ada.Real_Time;
with Ada.Text_IO; use Ada.Text_IO;

procedure Main with SPARK_Mode is
    Last : Time := Clock;
begin

    -- some stuff happening here ...

    if Clock > Last + Milliseconds(100) then
        Put_Line("Too late");
    end if;
end Main;

Clock 是一个有副作用的函数（每次调用它都会返回不同的值），在这个例子中，该函数用于所谓的“干扰上下文”（有关定义，请参见上面的链接）。

解决方案是稍微重写您的代码：

with Ada.Real_Time; use Ada.Real_Time;
with Ada.Text_IO; use Ada.Text_IO;

procedure Main with SPARK_Mode is
    Last : Time := Clock;
begin

    -- some code
    declare
        now : Time := Clock;
    begin      
        if now > Last + Milliseconds(100) then
            Put_Line("Too late");
        end if;
    end;
end Main;

因此，基本上，您所做的是将对具有副作用的函数的调用隔离到一个单独的语句中，将结果保存在一个变量中，然后使用您之前调用过的变量。这个技巧也应该有助于您调用受保护的对象。

于 2018-01-22T17:33:03.920 回答