arrays - Ada 和 SPARK 标识符 `State` 此时未声明或不可见

Question

我正在使用 SPARK 方法在 Ada 上进行自动列车保护。这是我在 SPARK 中的规范:

package Sensors
--# own State,Pointer,State1,State2;
--# initializes State,Pointer,State1,State2;
  is
    type Sensor_Type is (Proceed, Caution, Danger, Undef);
       subtype Sensor_Index_Type is Integer range 1..3;


  procedure Write_Sensors(Value_1, Value_2, Value_3: in Sensor_Type);
  --# global in out State,Pointer;
  --# derives State from State,Value_1, Value_2, Value_3,Pointer &
  --#                        Pointer from Pointer;
  function Read_Sensor(Sensor_Index: in Sensor_Index_Type) return Sensor_Type;

  function Read_Sensor_Majority return Sensor_Type;

  end Sensors;

这是我的艾达:

   package body Sensors is
      type Vector is array(Sensor_Index_Type) of Sensor_Type;
      State: Vector;

      Pointer:Integer;
      State1:Sensor_Type;
      State2:Sensor_Type;

      procedure Write_Sensors(Value_1, Value_2, Value_3: in Sensor_Type) is
      begin
         State(Pointer):=Value_1;
         Pointer:= Pointer + 1;
         State(Pointer):=Value_2;
         Pointer:= Pointer + 1;
         State(Pointer):=Value_3;
      end Write_Sensors;

      function Read_Sensor (Sensor_Index: in Sensor_Index_Type) return Sensor_Type
      is
         State1:Sensor_Type;
      begin
         State1:=Proceed;
         if  Sensor_Index=1 then
            State1:=Proceed;
         elsif Sensor_Index=2 then
            State1:=Caution;
         elsif Sensor_Index=3 then
            State1:=Danger;
         end if;
         return State1;
      end Read_Sensor;

      function Read_Sensor_Majority return Sensor_Type is
         State2:Sensor_Type;      
      begin
         State2 := state(1);
         return State2;
      end Read_Sensor_Majority;

   begin -- initialization
      State:=Vector'(Sensor_Index_Type =>Proceed);  
      pointer:= 0; 
      State1:=Proceed;
      State2:=Proceed;
   end Sensors;

我想知道为什么在函数 Read_Sensor_Majority 中我无法使用 State(1) 或任何 State() 数组值。如果有办法使用它们，我是否应该在 SPARK 的规范中添加任何内容来实现它？

它显示的错误是:

1)Expression contains referenced to variable state which has an undefined value flow error 20
2)the variable state is nether imported nor defined flow error 32
3)the undefined initial value of state maybe used in the derivation of the function value flow error 602

Answer 1

您需要更改规范才能读取

function Read_Sensor_Majority return Sensor_Type;
--# global in State;

正如我在上面的评论中所说，我很困惑

State := Vector'(Sensor_Index_Type => Proceed);

但是编译器接受它，所以它一定没问题。并且稍微测试一下，效果与

State := Vector'(others => Proceed);

还很高兴地报告，SPARK GPL 2011 工具集现已可用于 Mac OS X!