ada - SPARK 中的任务需要按顺序进行细化

Question

我目前正在大学实时编程语言类(class)中学习 Ada，并对 SPARK 有疑问。

我正在开发一个项目，其任务是监视离网电源。这项任务对于机器安全至关重要，因此应该尽可能没有错误，例如通过 SPARK 进行验证。

我收到一个奇怪的错误，我无法找到解决11:14 SPARK 中的任务需要顺序阐述(SPARK RM 9(2))违反 pragma SPARK_Mode

原始代码有点长，但我能够通过一个最小的示例得到相同的错误。

规范:

pragma Profile (Ravenscar);
pragma SPARK_Mode;

with System;

package simple_monitoring is

   function sign (val : in Float) return Float
     with Pre => val >= 10.0;

   task type myTask is
   end myTask;

end simple_monitoring;

实现:

pragma Profile (Ravenscar);
pragma SPARK_Mode;

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

package body simple_monitoring is

   function sign (val : in Float) return Float is
      res : Float;
   begin
      pragma Assert (val >= 10.0);
      res := 100.0 / val;

      return res;

   end sign;

   task body myTask is
      TASK_PERIOD : constant Time_Span := Milliseconds (100);
      next_time : Time := Clock;

      myVar : Float;
   begin
      loop
         Put_Line ("Running task");

         myVar := sign (20.0);

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

end simple_monitoring;

感谢任何帮助:-)

Answer 1

您需要额外的配置编译指示

pragma Partition_Elaboration_Policy (Sequential);

(参见ARM H.6)。对于您给出的示例，这只需要放在规范上；但一般来说，它需要是程序范围的配置编译指示。

您可以通过一个文件(例如 gnat.adc)来安排此操作，其中包含例如

pragma Profile (Ravenscar);
pragma Partition_Elaboration_Policy (Sequential);

并在 GNAT 项目文件的包 Builder 中引用它:

package Builder is
   for Global_Configuration_Pragmas use "gnat.adc";
   ...