Spark Proof аннотация

Question

Привет, я пытаюсь написать корректные аннотации от этой функции.. это написано с использованием языка программирования 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.

Answer 1

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

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

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

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

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

Answer 2

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

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

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

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

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

Barnes (ed. Выше) p.278 действительно показывает "функции доказательства", которые могут быть объявлены в аннотациях для этой цели. Их тела затем имеют доступ к внутреннему состоянию для выполнения конкретных проверок.

Answer 3

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

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

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