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

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

1 голос
/ 15 ноября 2011

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

Ответы [ 2 ]

2 голосов
/ 16 ноября 2011

Вам нужно изменить спецификацию на: 

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!

0 голосов
/ 15 ноября 2011

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

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

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

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

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

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

...