искробезопасный аннотацию

Question

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

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

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

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

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

Answer 2

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

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

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

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

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

Answer 3

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

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

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

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

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

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