1

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

2 回答 2

2

您需要更改规格以阅读

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！

于 2011-11-15T20:01:27.963 回答
0

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

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

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

如果我不得不对我在这里的信息进行疯狂的猜测，我会说它可能与你从State(1)例程中读取值有问题Read_Sensor_Majority，因为它无法知道你之前已经放置了一个值进入该阵列位置。

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

如果 SPARK 喜欢在甚至没有通过 Ada 编译器的代码上吐出“我很困惑”的错误，那么在让 SPARK 查看之前确保 Ada 编译器喜欢你的代码的纯 Ada 部分可能是明智之举超过。

于 2011-11-15T14:24:25.333 回答