Идентификатор Ada и SPARK `State` либо не объявлен, либо не виден в данный момент

Question

Я делаю автоматическую защиту поезда на Аде с помощью подхода SPARK. Это моя спецификация в 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!

Answer 2

Хех. Ну, это определенно ошибки SPARK, а не ошибки компилятора "garden garden".

Было бы неплохо увидеть фактическую версию ошибок (с указанием того, на какие строки они ссылаются), а не просто несовершенную транскрипцию. Тем не менее, я понимаю, что это не всегда возможно по соображениям безопасности / подключения.

Похоже, что все трое жалуются на поток данных через вашу систему. Не зная, на какие строки они ссылаются, лучшее, что я могу предложить, - это попытаться вручную проследить ваш поток данных через вашу систему, чтобы понять, в чем их проблема.

Если бы мне пришлось делать дикие предположения с информацией, которая у меня есть, я бы сказал, что, возможно, у вас возникли проблемы с чтением значения из State(1) в рутине Read_Sensor_Majorityпотому что он не может знать, что вы ранее поместили значение в это местоположение массива.

Код, который вы имеете в пакете begin...end Об этом должна позаботиться область тела, за исключением того, что, похоже, сама ошибка компиляции, как указал Саймон в комментариях. Возможно, если вы исправите эту проблему, SPARK поймет, что происходит, и перестанет жаловаться на ваши потоки управления.

Если SPARK любит выплевывать ошибки "Я в замешательстве" на код, который даже не проходит мимо компилятора Ada, может быть, стоит убедиться, что компилятору Ada нравится чистая часть кода Ada, прежде чем просить SPARK посмотреть его. над.