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;

这是我的Ada:

   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!

Answer 2

嘿。好吧，这些肯定是SPARK错误，而不是"普通"编译器错误。

看到错误的实际剪切和粘贴版本(以及它们引用的行的指示)而不仅仅是不完美的转录将会很好。然而，我确实意识到，出于安全/连接的原因，这并不总是可能的。

看起来这三个人都在抱怨通过系统的数据流。在不知道它们指的是哪一行的情况下，我的最佳建议是尝试通过系统手动跟踪数据流，以尝试查看它们的问题是什么。

如果我不得不对这里的信息进行大胆的猜测，我会说它可能与您在例程Read_Sensor_Majority中读取State(1)的值有问题，因为它无法知道您先前已将值放入该数组位置。

你在包的begin...end主体区域的代码应该照顾，除了它似乎有一个编译错误本身，正如Simon在评论中指出的。也许如果你解决了这个问题，SPARK就会明白发生了什么并且不再抱怨你的控制流。

如果SPARK喜欢在没有通过Ada编译器的代码上吐出"我很困惑"的错误，那么在要求SPARK检查之前，确保Ada编译器喜欢代码中纯Ada部分可能是明智的。