Ada 和 SPARK 标识符“状态”此时未声明或不可见答案

【问题标题】：Ada and SPARK identifier `State` is either undeclared or not visible at this pointAda 和 SPARK 标识符“状态”此时未声明或不可见
【发布时间】：2011-11-14 21:46:53
【问题描述】：

我正在使用 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

【问题讨论】：

(1) 我不知道 SPARK 工具集，但是错误消息没有给您一些提示吗？也许如果您发布它们，它会帮助我们帮助您。 (2) SPARK Ada 必须是合法的 Ada，但你最后对 State 的初始化不是。我想你的意思是说State := Vector'(others => Proceed);。 (3) 您的代码已经出现相当混乱，如果它更整洁，我们会帮助您！
在这里备份西蒙。我怀疑您的“我不能使用状态数组值”等同于普通编译错误。如果没有看到有问题的错误，我们真的没有什么可做的了。
好的，我在问题末尾添加了错误

标签： arrays function ada spark-ada

【解决方案1】：

您需要更改规范才能阅读

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

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

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

但编译器接受它，所以它一定没问题。并且小测试显示效果和

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

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

【讨论】：

【解决方案2】：

呵呵。好吧，这些绝对是 SPARK 错误，而不是“花园式”编译器错误。

很高兴看到错误的实际剪切和粘贴版本（以及它们所指的行的指示），而不仅仅是不完美的转录。但是，我确实意识到出于安全/连接原因，这并不总是可行的。

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

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

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

如果 SPARK 喜欢在甚至无法通过 Ada 编译器的代码上吐出“我很困惑”错误，那么在询问 SPARK 之前确保 Ada 编译器喜欢您的代码的纯 Ada 部分可能是明智之举去看看。

【讨论】：