Аннотация искробезопасности

привет, я пытаюсь написать аннотации для проверки этой функции .. это написано с использованием языка программирования Spark

function Read_Sensor_Majority return Sensor_Type is
       count1:Integer:=0;
       count2:Integer:=0;
       count3:Integer:=0;

      overall:Sensor_Type;

   begin


      for index in Integer range 1..3 loop
         if State(index) = Proceed then
           count1:=count1+1;
         elsif State (index) = Caution then
            count2:=count2+1;
         elsif State (index)=Danger then
            count3:=count3+1;
         end if;
      end loop;

      if count1>=2 then
         overall:=Proceed;
      elsif count2>=2 then
         overall:=Caution;
      elsif count3>=2 then
         overall:=Danger;
      else
         overall:=Undef;
      end if;

      return overall;

   end Read_Sensor_Majority;

   begin -- initialization
   State:= Sensordata'(Sensor_Index_Type => Undef);
end Sensors;

это файл .ads

package Sensors
   --# own State;
   --# initializes State;
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;
   --# derives State from State ,Value_1, Value_2, Value_3;

   function Read_Sensor(Sensor_Index: in Sensor_Index_Type) return Sensor_Type;
   --# global in State;

   function Read_Sensor_Majority return Sensor_Type;
   --# global in State;
   --# return overall => (count1>=2 -> overall=Proceed) and
   --#                   (count2>=2 -> overall=Caution) and
   --#                   (count3>=2 -> overall=Danger);


end Sensors;

это ошибки, которые я получаю после проверки файла с помощью искрового экзаменатора

Examiner Semantic Error   1 - The identifier count1 is either undeclared or not visible at this point. <b>34:27</b>     Semantic Error   1 - The identifier count1 is either undeclared or not visible at this point. Examiner
Sensors.ads:34:27
Semantic Error   1 - The identifier count1 is either undeclared or not visible at this point.

ada spark-ada
person mohammad Mustafa    schedule 17.11.2013    source источник
comment
Почему это помечено как java??   -  person    schedule 17.11.2013
comment
очевидно, потому что есть какой-то инструментарий Java под названием Spark. Не путать со СПАРК! Теги Java и C++ кажутся здесь неправильными.   -  person user_1818839    schedule 17.11.2013

Ответы (3)


arrow_upward
2
arrow_downward

Вы должны объявить идентификаторы, прежде чем сможете ссылаться на них (за некоторыми исключениями).

Что наиболее важно, базовым принципом как SPARK, так и Ады является то, что спецификации могут обрабатываться без каких-либо знаний о возможных соответствующих реализациях.

Поскольку ни overall, ни count1, count2 или count3 не объявлены в спецификации, вы также не можете ссылаться на них там.

Два небольших примечания:

  • Пожалуйста, используйте тот же стиль идентификатора, что и в справочнике по языку. (Начало в верхнем регистре, подчеркивает разделяющие слова.)
  • Почему Sensor_Index_Type является подтипом Integer?
person Jacob Sparre Andersen    schedule 18.11.2013

arrow_upward
1
arrow_downward

Просто сам играю со SPARK, так что это не полный ответ.

(Стоит упомянуть, какой СПАРК, так как существуют разные версии, и СПАРК-2014, кажется, немного отличается от других) В настоящее время у меня есть только версия 2006 года Barnes, который не охватывают последние версии.

Основная проблема совершенно очевидна: предоставив абстрактное представление о состоянии пакета --# own State; в спецификации, вы не можете затем проникнуть внутрь и наблюдать за спецификой.

Что с этим делать, мне не совсем понятно, но имеет наметочную форму: предусмотреть более абстрактную форму постусловий для Read_Sensor_Majority в спецификации, а конкретную форму перенести в тело.

Один из подходов, принятых в Ada-2012 (не знаю, насколько он применим к Spark-2005), заключается в предоставлении в спецификации дополнительной функции function satisfies_conditions (...) return boolean;, которую можно вызывать в аннотациях и тело которой содержит конкретную реализацию.

Барнс (изд. выше) стр. 278 действительно показывает «функции доказательства», которые могут быть объявлены в аннотациях для этой цели. Затем их тела имеют доступ к внутреннему состоянию для выполнения конкретных проверок.

person user_1818839    schedule 18.11.2013

arrow_upward
0
arrow_downward

Учитывая, что вы показываете файлы .ads и .adb, я отмечаю, что доказательство в файле .ads ссылается на элементы в теле. Может быть, прувер не может проникнуть в тело и извлечь эти переменные? (то есть проблема видимости.)

Сообщение:
The identifier count1 is either undeclared or not visible at this point.
Кажется, это указывает на то, что дело обстоит именно так.

Я не знаю SPARK, так что это мое лучшее предположение.

person Shark8    schedule 17.11.2013
comment
да, я думаю, что это проблема .. но я не знаю, как это исправить. - person mohammad Mustafa; 18.11.2013
comment
Может быть, перенести аннотации в тело? - person Shark8; 18.11.2013